{"entities":{"Q2945654":{"pageid":2956374,"ns":120,"title":"Item:Q2945654","lastrevid":85130042,"modified":"2026-06-03T05:59:37Z","type":"item","id":"Q2945654","labels":{"en":{"language":"en","value":"Deriving comparators and show functions in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6481879"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$10FCE9A5-FA38-4E6C-86CE-04A5880E29AB","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c5118373b06d1acd889db3534e9c3f69a03595ac","datavalue":{"value":{"text":"Deriving Comparators and Show Functions in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q2945654$892045E0-80E9-4313-8170-C6569C8364EB","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"ef0fbc7cce1a865ac69547f0e6ec539af53b806a","datavalue":{"value":"1465.68063","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945654$B686DFC3-35BD-475D-8E46-EC68A03D7EA0","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"07ea93b48f6a339a8a93afd26dad0f71c5ff2b1d","datavalue":{"value":"10.1007/978-3-319-22102-1_28","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945654$AF0E85C2-F45B-4AF1-9304-0A5EA17978B0","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0653fc883593f9e70c5ddda3d1f1f752c0d0ffca","datavalue":{"value":{"entity-type":"item","numeric-id":530846,"id":"Q530846"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$7CD4D845-7AB5-4766-9E94-2F83DBA5E0D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"c8e2771b20e3c98dace74591de69baf1cddaba7f","datavalue":{"value":{"entity-type":"item","numeric-id":515686,"id":"Q515686"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$63B84ABF-4AF6-499D-BCC8-D49494BE8182","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"d43c6ce6e92d67a2cb7e4a7df2a7d5eeec36e724","datavalue":{"value":{"entity-type":"item","numeric-id":2829237,"id":"Q2829237"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$22757EB8-2D15-4502-B715-0BF257CFA188","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ece460bc202bb4ec344b5d620998e472753b138b","datavalue":{"value":{"time":"+2015-09-14T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q2945654$3485FD66-C8D3-4623-B317-B606BFA4D6B7","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"14cf74de25853c940589b125137b792dfb2d092b","datavalue":{"value":"68P05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945654$3114AD4E-DE43-4CFD-B18C-7E2368A06DF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945654$8B4F19A6-BB07-43F6-8C21-8DCB9E53EC1F","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"cb30586e566c8fce0b78a6bed17dfacb5eebfe0f","datavalue":{"value":"6481879","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945654$4E52A861-A9BE-4016-89DD-8102799E0222","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c5fcda2c98ddff866834785339eb37077e5eb1fe","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$5E9D5B7B-B356-48A3-8654-405EF948B2F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"7f231912461a4cf859d87b4356c5e2a2037e1e84","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$C3107B85-AC18-43DD-A16C-8DFB7EF92CCD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"067e00213990a6f2431e78667be3f10443c92f4f","datavalue":{"value":{"entity-type":"item","numeric-id":16052,"id":"Q16052"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$8187B9BF-ED98-449C-BA67-E58380F7F3B5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8e7deacad56e3bf59f522de6c1fa96858f2fd494","datavalue":{"value":{"entity-type":"item","numeric-id":18676,"id":"Q18676"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$A5B2C056-F9FC-4E2A-88F6-F133C9E42E34","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"fa5dc13872ba1592e71dabc4befba1daea72a8a3","datavalue":{"value":{"entity-type":"item","numeric-id":14275,"id":"Q14275"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$4D7132F8-A531-4CBB-88F7-CAEC93E95D24","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$6F8E4C83-DEC7-4C9D-9998-B15EDB50BFDF","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"ae4648756d1b788d14fb11f73a62e07a669f084c","datavalue":{"value":"https://doi.org/10.1007/978-3-319-22102-1_28","type":"string"},"datatype":"url"},"type":"statement","id":"Q2945654$C4B14712-95FB-418F-B743-F47E154AA5F5","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"dd270e8af2b3bafe1d344be063e9eae15fc75062","datavalue":{"value":"W2407034734","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q2945654$0B1C3BD9-61B6-4CBC-BB05-17DD178D0336","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"d4d993f7be3ea77cad4a800be898a39b5ce70ed5","datavalue":{"value":{"entity-type":"item","numeric-id":2879246,"id":"Q2879246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$FF147BB3-C3A3-4D27-B475-7D28340D3440","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"931c42c28f22f89fe1b66164f9ececc2021ac1a2","datavalue":{"value":{"entity-type":"item","numeric-id":3558332,"id":"Q3558332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$F1097CF6-EDCF-429C-9027-ACFA63C03052","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"62952827b65adcfbdb658bf4a88dcb63d7865607","datavalue":{"value":{"entity-type":"item","numeric-id":4921511,"id":"Q4921511"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$94E4FFAF-8D3A-4F43-98A1-D08EF8956F3D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"0f0278a622341c2c3ea684f66af68a5b07b0b894","datavalue":{"value":{"entity-type":"item","numeric-id":972425,"id":"Q972425"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$BBB6F33A-23F6-4FDD-8C07-CD8A13A9FF62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"22a5a326924c9f9f3cf0f5061fb0ff950ccfad0d","datavalue":{"value":{"entity-type":"item","numeric-id":5747660,"id":"Q5747660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$B0C77F6E-EB11-47CE-9604-E19F09F65EE0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a7a1ce015f9a6115f5e15ce96a4b6a73ac4d89f9","datavalue":{"value":{"entity-type":"item","numeric-id":5327340,"id":"Q5327340"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$CA7A886E-C733-4D31-B70B-7F82B53590DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"84afe353d96a988928bd5d41e96afba7e81d6980","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$C544E5B3-5069-429E-9D01-11ED09FFD3FF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"412793878c356c2acdccde0f6f22f73f790f84b2","datavalue":{"value":{"entity-type":"item","numeric-id":3559762,"id":"Q3559762"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$A0A8148B-3AF2-4198-B6D7-0086905C8B50","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b0aef60bd392ccfb5e82daa98f095917b33d1745","datavalue":{"value":{"entity-type":"item","numeric-id":3183545,"id":"Q3183545"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$36732F9A-8C52-410A-B7C5-075E00750940","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c2fa401b3f58fb4c2bc9ea2f71ee0d728db11587","datavalue":{"value":{"entity-type":"item","numeric-id":2986838,"id":"Q2986838"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q2945654$8DA4FE01-1C56-434D-9A14-65EA0105913D","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9c977d5da30781aedab959d3b8317c7b9eca99d9","datavalue":{"value":{"entity-type":"item","numeric-id":5327339,"id":"Q5327339"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"074222ee6efd1f3c5b0bbbae8f748dde82e110e0","datavalue":{"value":{"amount":"+0.7377633452415466","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2945654$4797EBF5-0555-49A1-9675-EA5E8BF07B5F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"38394b4e8d3a3502630a463829cd1f4840ac5524","datavalue":{"value":{"entity-type":"item","numeric-id":3172879,"id":"Q3172879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c062184591919016c333779c20099c6ace0d1868","datavalue":{"value":{"amount":"+0.6852952837944031","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2945654$42B1DAFB-BC00-4E28-BDC8-3B2153B17421","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1c8b9f7343efe63e57ddd2bd2ef0ae5831271484","datavalue":{"value":{"entity-type":"item","numeric-id":2324018,"id":"Q2324018"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"85d2355e6e50a8f75286412f0ed7cafb0337b4f4","datavalue":{"value":{"amount":"+0.6836877465248108","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2945654$8EE3D058-8663-4A93-A98B-6606D6AF4771","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"fe48151ebb376d54c8f462ba2eabb814b6e0efc4","datavalue":{"value":{"entity-type":"item","numeric-id":3558332,"id":"Q3558332"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"98d511ae2ac3fe1422276a6b1dd38131f1d22bea","datavalue":{"value":{"amount":"+0.6796813607215881","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2945654$00031E51-0983-40EA-B535-5A63C5D4E67F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"408e6eb37370f869866c0d5e2e591da6ab9b54f4","datavalue":{"value":{"entity-type":"item","numeric-id":3613430,"id":"Q3613430"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6cb596415a4f19d2779a251791b4506d801485d5","datavalue":{"value":{"amount":"+0.6773406267166138","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"a327a09ea0305e98d5cf33bd4036320e19f2aed0","datavalue":{"value":{"entity-type":"item","numeric-id":6821328,"id":"Q6821328"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q2945654$4D66E097-CC10-4F5C-B1FE-5414DCCD4C15","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Deriving comparators and show functions in Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Deriving_comparators_and_show_functions_in_Isabelle/HOL"}}}}}