{"entities":{"Q4933332":{"pageid":6962914,"ns":120,"title":"Item:Q4933332","lastrevid":51101822,"modified":"2026-01-16T16:33:37Z","type":"item","id":"Q4933332","labels":{"en":{"language":"en","value":"An Isabelle-like procedural mode for HOL Light"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 5798922"}},"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":"Q4933332$A47FCCD7-DF39-4AAB-AC1A-B3B4E313664B","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"903ca725314dc7daeb66ee140c627d21adf08bab","datavalue":{"value":{"text":"An Isabelle-Like Procedural Mode for HOL Light","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q4933332$373BD7CF-C901-49A0-8ADF-449A4D708079","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"c38caeee2f338ab5f69963cfca504ef8394d0ea6","datavalue":{"value":"1306.68149","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4933332$33ED2BE8-5A50-4E46-B0DD-FEAE71232EEC","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b11cd8e11c444a986f1993fe8f0444263e479723","datavalue":{"value":"10.1007/978-3-642-16242-8_40","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4933332$A1C6CF33-2148-4BB2-9253-F6CA2F7C0192","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"3973f059c1b5dc91d7940419c6f061f7ab77fe4d","datavalue":{"value":{"entity-type":"item","numeric-id":2405261,"id":"Q2405261"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4933332$8DD74ABC-ADBF-495E-AB5A-CF29BB832FF4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"8d78e8b1fd2bada0896418639974db329feb4fe3","datavalue":{"value":{"entity-type":"item","numeric-id":2102945,"id":"Q2102945"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4933332$C64991E9-CE0E-4D17-B5AE-7480830E9482","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"23864e2be568bb8a6a4b0526f5a5216348320070","datavalue":{"value":{"entity-type":"item","numeric-id":2870110,"id":"Q2870110"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4933332$56CC22C1-248A-472C-8865-0CD51122B12C","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"8268186a71ffa78cd296b9bac558860fe9e35f3f","datavalue":{"value":{"time":"+2010-10-12T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q4933332$D35AC411-5F1C-4210-928B-2CBEE7DA6527","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4933332$481CC572-D1E8-4806-8175-E88FBFC1D7E5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"737dfb432da6cb4b9ff9b2f05e0b004d455b198a","datavalue":{"value":"5798922","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4933332$8896B4C9-9A7C-4D03-8B3D-5145D48B822E","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ab6ee58efeeaa685ac2b8ecf828badcfb673e8c7","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4933332$7C5A7581-C858-4C6A-A946-96C7F627EF2A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ee80fa482e8c030191fc3263e069d0dc0cdf7815","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q4933332$D0E02690-9A4B-4C01-A8CD-79EDE2854E8B","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":"Q4933332$79CFA828-08E6-4014-9490-E57064435E30","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":"Q4933332$DDB23C09-B4E4-4C3A-9613-4A8572A27510","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"c4368b1c9755c3db3ae99c172c44c15c5259d93d","datavalue":{"value":"https://doi.org/10.1007/978-3-642-16242-8_40","type":"string"},"datatype":"url"},"type":"statement","id":"Q4933332$FBD65D36-C3D3-4E35-BAFD-7C0EB48AE986","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"7a368d04ad586ad84e2e4f99ca41f4a81faeaa6a","datavalue":{"value":"W1483802687","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q4933332$D4374A3A-247C-49B5-B3B4-BD2B113F9E76","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"f5240345605b6df958dc529fb8dc1a54b30d31b3","datavalue":{"value":{"entity-type":"item","numeric-id":3183517,"id":"Q3183517"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"dfe23d5b017aa876a29e70ec2902d5102fdacecb","datavalue":{"value":{"amount":"+0.7672960758209229","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":"Q4933332$6C0351C9-2C65-4EC6-9ED9-A995AD847FA3","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":"22ce72491243dae90e6d138e02b1277cd9eecef6","datavalue":{"value":{"amount":"+0.7412963509559631","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":"Q4933332$2499DABA-FDB3-48C6-8BC8-E3B48908D63D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"20821278b54273bce32a61f8d97e3bf2e0967751","datavalue":{"value":{"entity-type":"item","numeric-id":5307074,"id":"Q5307074"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"2632134322eb07ebaa7a8d602aeb2587f2c2b209","datavalue":{"value":{"amount":"+0.7041814923286438","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":"Q4933332$A76872E5-89E7-4991-9D25-BFF8AE5FA029","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"895f01dbe4514afaf4e58308193c557e5a7e265f","datavalue":{"value":{"entity-type":"item","numeric-id":2375439,"id":"Q2375439"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"4e2d99605fc1c73c0b19533f4ffdc276f7ae9270","datavalue":{"value":{"amount":"+0.7006182670593262","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":"Q4933332$A4B77DDF-E0B4-40D7-AF29-4C1DDDC4334B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"952dd0313ffcdf0b91b490f0739b8e7d073d048d","datavalue":{"value":{"entity-type":"item","numeric-id":3454108,"id":"Q3454108"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"9dd561a27445f6ff50684cd588e3e2d373366e36","datavalue":{"value":{"amount":"+0.6995413899421692","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":"Q4933332$857AB3DB-C9EA-4621-A6BF-3F485EBAAC7B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:4933332","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:4933332"}}}}}