{"entities":{"Q287365":{"pageid":289132,"ns":120,"title":"Item:Q287365","lastrevid":60714777,"modified":"2026-04-10T18:41:21Z","type":"item","id":"Q287365","labels":{"en":{"language":"en","value":"Eisbach: a proof method language for Isabelle"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6585634"}},"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":"Q287365$8C16F9AC-4A24-441F-9EEC-189F41C1AD90","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"406085d79dd11ccc9001a5dab52442995a55b603","datavalue":{"value":{"text":"Eisbach: a proof method language for Isabelle","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q287365$0EA2C968-D19A-403D-8A1D-018F216ECFCA","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"0a48970b49addc788bd55d67084f82bdcc2b3546","datavalue":{"value":"1356.68195","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287365$28452B64-79C1-4EB1-BAB2-8A7D79A69425","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"5fbfbec2406713b1ee2886412d7c8dd091cd9c18","datavalue":{"value":{"entity-type":"item","numeric-id":287362,"id":"Q287362"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$CF5DAC38-F540-478D-AD1F-B88C959DB1F6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"45e6c2a5937a40e685c427c9b959ad4c359ca8cc","datavalue":{"value":{"entity-type":"item","numeric-id":287363,"id":"Q287363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$A0350332-7501-4272-8246-8AF7958F74F5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"a162d67ca0f0da05fadb758011f7efa5d1e07db6","datavalue":{"value":{"entity-type":"item","numeric-id":287364,"id":"Q287364"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$AE25AD80-04FE-488C-BC4C-C17293E42C95","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"b84cc8b5923f45dc86ae69f67f68bf56d7ecfce9","datavalue":{"value":{"entity-type":"item","numeric-id":174771,"id":"Q174771"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$AD82B1FC-4A4E-486C-829D-5047AA4AEA52","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"b626bb78b3e93b3076e6958296f7f25e2e74c3ab","datavalue":{"value":{"time":"+2016-05-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q287365$987EF56A-BD34-429D-A345-5453534D3D2B","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287365$524EDAC7-27B3-44F1-8CD4-B6523DB139FB","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"d97997171e7096c9dedb0eab4ddaeeeb32a66057","datavalue":{"value":"6585634","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287365$A3B26D84-8B7C-4339-B996-D7FAB9B40D01","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q287365$0AF4C790-6540-4D64-B94B-6123621BD42C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d39e48c43b0ad9cc4fdda6c12c172f8c3758d167","datavalue":{"value":"Eisbach","type":"string"},"datatype":"string"},"type":"statement","id":"Q287365$774CE81B-C64C-4AB1-A16A-E2D13944D167","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"d62798ced101241ac0d5e46110e32d69e73a0c1a","datavalue":{"value":"proof automation","type":"string"},"datatype":"string"},"type":"statement","id":"Q287365$0E40AD84-5C5D-488D-BDE6-76628FE9954D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"e9b4798624a5c5ff39495ac81b083ac165a6d082","datavalue":{"value":"seL4","type":"string"},"datatype":"string"},"type":"statement","id":"Q287365$60DD2302-76CD-4026-A7AA-02B776B0D4B4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"71d28794fc8bcc0518a22c59d95b1e5e7c580da5","datavalue":{"value":"l4.verified","type":"string"},"datatype":"string"},"type":"statement","id":"Q287365$64966CA6-768E-4FF6-88C9-3462DCCD88E9","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ae4173d13b960594f2bf5bfd22402fc0202f2b76","datavalue":{"value":{"entity-type":"item","numeric-id":40255,"id":"Q40255"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$D69F4007-A217-414F-8A43-C21E57BC4628","rank":"normal"},{"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":"Q287365$3AB96741-8088-411D-88A0-E8608F21854C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"25db55153babd7076d594d911b639e78d62b451a","datavalue":{"value":{"entity-type":"item","numeric-id":20369,"id":"Q20369"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$ECDC9F32-DD45-4E2D-A826-2E624591938C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"2ad21f150c621099eebc7c2e673cd9cf43b81a4e","datavalue":{"value":{"entity-type":"item","numeric-id":24376,"id":"Q24376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$E1B7BCC7-1DCD-4B00-9B5E-05A5A587B1F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c2e87d897ce5d80b030b7930ad6e7942edbeeaaf","datavalue":{"value":{"entity-type":"item","numeric-id":24996,"id":"Q24996"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$1A53E8E5-67B9-43AE-919A-EDFA11E95569","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"d4f20857e79be9881c5d7a06583454f1cf2611e9","datavalue":{"value":{"entity-type":"item","numeric-id":24994,"id":"Q24994"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$5FE76E53-9231-46AD-A2CC-12F4F050EE59","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"a94daa7865c51c0d2412cced8422ea9361d06e30","datavalue":{"value":{"entity-type":"item","numeric-id":21343,"id":"Q21343"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$4A472B14-4AAC-4590-8680-56D131A849A3","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":"Q287365$6B61B9A6-4845-454B-A838-4807F9306716","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"19db008058ce3a679389c190541b4b00e350555f","datavalue":{"value":{"entity-type":"item","numeric-id":27113,"id":"Q27113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$FF89D486-F505-4049-AC7B-D39FF9A02C1D","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":"Q287365$A18F6C8E-7D8D-4717-A521-312831B31BDA","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"0a76f869dbc2f54420f40c561acdbe2a42bb803f","datavalue":{"value":"https://doi.org/10.1007/s10817-015-9360-2","type":"string"},"datatype":"url"},"type":"statement","id":"Q287365$A2354302-1275-4DFA-BEB1-681BFC37EBDD","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"e2da72ed76190f38de7071ec928e4d19c07c5af6","datavalue":{"value":"W2290529759","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287365$0DCE6B8D-1DF7-4F68-A9D7-622EE05E9022","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"7a655377852f4fbc1e40cdceec18686655bda680","datavalue":{"value":{"entity-type":"item","numeric-id":5712320,"id":"Q5712320"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$EF944463-7C71-47CC-BC81-032C1AC7C343","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a4738798d9702e646d9743f53f948745583da971","datavalue":{"value":{"entity-type":"item","numeric-id":2352487,"id":"Q2352487"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$447F654C-316A-4D59-AED0-9DAF596981AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ea807940fd1e67ba0ae2d30da1a0644b63db761d","datavalue":{"value":{"entity-type":"item","numeric-id":2907311,"id":"Q2907311"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$89B44EF2-1780-4F8B-8773-72115966E07D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"a386259d7b6de278f96d59178a0ebe00c941a927","datavalue":{"value":{"entity-type":"item","numeric-id":3543657,"id":"Q3543657"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$E8393576-9A1E-463B-A9F4-638D17E3BBA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"526569e2045d88153ecb5cf7f75a680cdcd5a85b","datavalue":{"value":{"entity-type":"item","numeric-id":2767010,"id":"Q2767010"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$BF25C8B0-DF09-4615-8BFC-0D442933D617","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"d43f11a5e6fc21caa581e9ac1e35682b1839d73e","datavalue":{"value":{"entity-type":"item","numeric-id":3075246,"id":"Q3075246"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$188292B7-474B-4153-B16F-79193FD76AC9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"adaff45a41d0a6bdbe56b77312c8af13a691189a","datavalue":{"value":{"entity-type":"item","numeric-id":5398327,"id":"Q5398327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$5C890263-03AF-462B-B735-2B5F13C9B60F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6cc8abb92210655a5bd4143cbbadd6eadb52d635","datavalue":{"value":{"entity-type":"item","numeric-id":1801222,"id":"Q1801222"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$5EE53D0A-A7C5-49BC-A0A1-D189828B01C6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"c8bfb4cfac567a097f2a651df3bdc8285a6e2cdc","datavalue":{"value":{"entity-type":"item","numeric-id":2945633,"id":"Q2945633"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$BDD59A8C-EA98-480D-AAC7-F17018643BD5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5cdda75f152e068016ce6e94687febfaf56ec336","datavalue":{"value":{"entity-type":"item","numeric-id":2879265,"id":"Q2879265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$D35FC33B-5184-435F-BB53-A2625F1BF323","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"69c3e9d2aaa3b076c04e44188e92a5a39a71ffde","datavalue":{"value":{"entity-type":"item","numeric-id":4916056,"id":"Q4916056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$8604D1AD-4E85-491B-9C4D-E9DFFBB2A93B","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":"Q287365$3888DC5A-1DB8-4F42-81B6-48C7289C7E39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b42dd317bf0bbf239e78b0f994d050b3a8511fe5","datavalue":{"value":{"entity-type":"item","numeric-id":5244791,"id":"Q5244791"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q287365$09551BF5-DF2E-4E46-9A62-0BA883B09179","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"344a2899a980084996364d25edf50fd4c03f0994","datavalue":{"value":"10.1007/S10817-015-9360-2","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q287365$C4216D43-CD51-405F-88AF-5E5A5045B838","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b343ddeb7b8723940bff14faa8c0877850c55d01","datavalue":{"value":{"entity-type":"item","numeric-id":2879265,"id":"Q2879265"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"07bbfe62b6870c59b243cbf7152f65d9e13ab952","datavalue":{"value":{"amount":"+0.9283197","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287365$C698FEE6-3E0A-40D2-AE61-DF2D4FF0E0AC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"e1aac3c3e28f3c5c8a5eba2ddfcb1c23067c2156","datavalue":{"value":{"entity-type":"item","numeric-id":2405272,"id":"Q2405272"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2420d60c873d3ea62fe406448034ed216c732505","datavalue":{"value":{"amount":"+0.8830893","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287365$A87E6225-D14E-4F42-8CE0-2C0422949237","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"a50ad8a3efeeccd952f15206d6520ed593ff8b29","datavalue":{"value":{"entity-type":"item","numeric-id":5756773,"id":"Q5756773"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6a7716ae970d03f3555145485cba7dd5e15ba12d","datavalue":{"value":{"amount":"+0.88150597","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287365$555BE8A4-F716-49BC-9B4F-94336AA6874F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"2354685b260f18674ebd054e43dc88ce09d927c7","datavalue":{"value":{"entity-type":"item","numeric-id":2055847,"id":"Q2055847"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"15099a325b062f62992e17d823effbad960f077f","datavalue":{"value":{"amount":"+0.8790644","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287365$AAC40AF1-AA7F-444B-B36C-E8F4D47F0255","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"353f83759ee34b781b1cadc49c3f90042799760c","datavalue":{"value":{"entity-type":"item","numeric-id":5200122,"id":"Q5200122"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c53757c86e50a4cda9f3f1c97051cf94903bc35a","datavalue":{"value":{"amount":"+0.872171","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287365$9DA0382F-6A2E-45D4-BC96-F8B1AEDE5E92","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"0783d322e8f85ae9785210c3d8bd9cdfc4bc9de5","datavalue":{"value":{"entity-type":"item","numeric-id":2055899,"id":"Q2055899"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8a1d90fb6910b6ee7fb19d39aa534d82966710d1","datavalue":{"value":{"amount":"+0.8720859","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287365$8D735B55-DF2A-4F61-87F3-504B12571EE1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"de589e3e2af4ab283fef3b323d16a0e4d7eeb181","datavalue":{"value":{"entity-type":"item","numeric-id":5713934,"id":"Q5713934"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"35f55273d9703153e2c22eee85c87293fa2f4c9d","datavalue":{"value":{"amount":"+0.87148976","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287365$F5712370-9373-40A5-970F-66E9DA8C3F4B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"7a3f82df12b0d518b03d54ec2b03e9ec5b8b222a","datavalue":{"value":{"entity-type":"item","numeric-id":1825045,"id":"Q1825045"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"ed79caa8246cef83661fe8a2e31485a6666a41ee","datavalue":{"value":{"amount":"+0.87120616","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287365$D1016806-4D21-4857-9A4B-A85AD0C288CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"9d8c676f8538b024eb2a80be0edde23296e2c1db","datavalue":{"value":{"entity-type":"item","numeric-id":1600086,"id":"Q1600086"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"79539a2c4e0ce2ac79091f2619ea523777d5d66b","datavalue":{"value":{"amount":"+0.87084484","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287365$7F481192-B664-4D8F-9FEE-7660CDA6174B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ed8aba500f89cbf727442fbde664c82a20d58a91","datavalue":{"value":{"entity-type":"item","numeric-id":2108191,"id":"Q2108191"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"03d2496c20e374e8b9d146054c4bf12445b3da34","datavalue":{"value":{"amount":"+0.8696588","unit":"1"},"type":"quantity"},"datatype":"quantity"}],"P1660":[{"snaktype":"value","property":"P1660","hash":"ac3c626774dcd0d16f89557f66586245841a01db","datavalue":{"value":{"entity-type":"item","numeric-id":6767936,"id":"Q6767936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"}]},"qualifiers-order":["P1659","P1660"],"id":"Q287365$90B4664C-21D8-4F7D-8049-9182AE7F0857","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Eisbach: a proof method language for Isabelle","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Eisbach:_a_proof_method_language_for_Isabelle"}}}}}