{"entities":{"Q1791180":{"pageid":1801922,"ns":120,"title":"Item:Q1791180","lastrevid":53218811,"modified":"2026-01-24T12:01:39Z","type":"item","id":"Q1791180","labels":{"en":{"language":"en","value":"Fast machine words in Isabelle/HOL"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 6946992"}},"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":"Q1791180$DBC7A078-6546-4F8B-BBC0-177F3F0CF4B0","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"45c588c532d265610808a2b14e539626997fa5ee","datavalue":{"value":{"text":"Fast machine words in Isabelle/HOL","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1791180$33E06F24-7A89-473A-84F9-1397443D3531","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"c915193b94045007e9f367c8f38f7e36ff2109c3","datavalue":{"value":"10.1007/978-3-319-94821-8_23","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791180$7A351C98-54B9-421D-8675-C8B44A69F1EE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b18da065d50ce37e447f1f6708524421ab8f031f","datavalue":{"value":{"entity-type":"item","numeric-id":1663232,"id":"Q1663232"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791180$16ED93E4-92A6-457A-876D-75310F5A3B54","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"ff3c7136492fcf13c84b92efb7ac37b3eed57322","datavalue":{"value":{"time":"+2018-10-04T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1791180$A8885EEC-09DF-4889-B190-1DC997898F9A","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"a360651f48fb3ab31a1af8c50bb3f3739a50e7d8","datavalue":{"value":"68V15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791180$FF3A9C1B-51A8-4D0F-B4C2-D84330AC8082","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5ec63243674f665c4fb8c147a6c6d9e39f607ff1","datavalue":{"value":"68N30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791180$BF89C5E6-FD08-4570-9C4C-A916D3296CC5","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"dea8e489545272b0c0b563e8ca96b8df03e72669","datavalue":{"value":"6946992","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791180$98956BC9-6063-4708-AF9B-CC436AA8FBB9","rank":"normal"}],"P1463":[{"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":"Q1791180$CE3218A5-335D-4863-B3B7-B1F7936408AD","rank":"normal"},{"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":"Q1791180$866C0F7A-654F-4F14-80EA-BB69D7C366AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"ebe6f223efc2405cf071214b7d4e0e7858bf57fc","datavalue":{"value":{"entity-type":"item","numeric-id":18367,"id":"Q18367"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791180$1EA0EDF1-2E2A-4821-B23C-5F4E7CF64BCC","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":"Q1791180$FABC0751-7829-47A8-88EE-19E564AD69BE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"533959f24a509b955614f607e46b8aa4cec190ef","datavalue":{"value":{"entity-type":"item","numeric-id":20799,"id":"Q20799"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791180$D52A7B0F-88CA-4830-B6DD-FD66814C35C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"0d73b7a66c046be888f26faeb5ba8bce261b6bda","datavalue":{"value":{"entity-type":"item","numeric-id":29573,"id":"Q29573"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791180$F7D23AF5-3B8D-407D-9F8F-F40429BB4BE6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"8859dd07b075ca56b99edd7026e1e517c43d961e","datavalue":{"value":{"entity-type":"item","numeric-id":33165,"id":"Q33165"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791180$763920D1-3EF8-49A0-9EDE-8A45BC8F7DE9","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"56e7f84524c61979eec661db7577d9112d85d0eb","datavalue":{"value":{"entity-type":"item","numeric-id":33768,"id":"Q33768"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791180$73F71EE7-30DD-4474-938A-775D23092160","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"3edcee9066c8af5560373e04318011aa326faffb","datavalue":{"value":{"entity-type":"item","numeric-id":14483,"id":"Q14483"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791180$65748AD0-3700-4D58-8013-DA73CF889DA8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"c46d84e301480ba8a5854ea89c3d27b865a03eb9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791180$E94B15DB-DB3A-4260-A74F-8AD55AE88672","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":"Q1791180$0D7FCD0D-45A9-478F-940E-727D4BF310D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"6afb9e05f24776a03d7fcd415baf7b99112468c9","datavalue":{"value":{"entity-type":"item","numeric-id":34519,"id":"Q34519"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1791180$07279655-2091-4C8A-AC71-D7F6F8373297","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":"Q1791180$46AD3A50-F0AC-4786-A397-D866709E2E89","rank":"normal"}],"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"b161c3adf927f4a8a0a7695bf338e4ba5871dba7","datavalue":{"value":"https://doi.org/10.1007/978-3-319-94821-8_23","type":"string"},"datatype":"url"},"type":"statement","id":"Q1791180$1D0A5F8E-EC3D-4B79-9F2B-8F316296EDD4","rank":"normal"}],"P388":[{"mainsnak":{"snaktype":"value","property":"P388","hash":"94e77b80cf374cd9fd75089b193da25bbba90fdc","datavalue":{"value":"W2810581008","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1791180$AC3BD984-B9AD-4611-8FE4-DA0AB92EA5AD","rank":"normal"}],"P1643":[{"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":"a5e2d0dc78d42882372e3a591753b226fa9419f4","datavalue":{"value":{"amount":"+0.7212358117103577","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":"Q1791180$86C6A151-6008-4BE2-9E3F-6346D639F40A","rank":"normal"},{"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":"5959a8d4218b92358ef93616e4ef4d8f84072fca","datavalue":{"value":{"amount":"+0.7184590101242065","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":"Q1791180$AA1593BD-5E2A-4376-B302-6963D3125005","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"b08efbbf9ea68d31aeddb1977d895fd94a212ea3","datavalue":{"value":{"entity-type":"item","numeric-id":5747660,"id":"Q5747660"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"8c836cbabaed4ca5091ae46f3724b3f21eba5d20","datavalue":{"value":{"amount":"+0.7178622484207153","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":"Q1791180$70D89FE8-5872-4A22-98A3-504D93830215","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"c0df1a19b75f713e250e2c10008c5ee73c5afacb","datavalue":{"value":{"entity-type":"item","numeric-id":832940,"id":"Q832940"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"c2a584d659b5f49439be1f76ee13117b5fbef16d","datavalue":{"value":{"amount":"+0.7110722064971924","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":"Q1791180$FED79132-0DF4-499F-B1A2-5DDA6272F36F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"5f6828a02bb1974cc42923cc5d4b695ac187d5f0","datavalue":{"value":{"entity-type":"item","numeric-id":3613409,"id":"Q3613409"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6d4de59f1191d0d7a0d5c289f1962c6bd0140cde","datavalue":{"value":{"amount":"+0.700148344039917","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":"Q1791180$D9A8F952-8C7B-4572-9728-43DF3AB0FB6E","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Publication:1791180","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Publication:1791180"}}}}}