{"entities":{"Q1312157":{"pageid":1322907,"ns":120,"title":"Item:Q1312157","lastrevid":67141644,"modified":"2026-04-12T15:34:04Z","type":"item","id":"Q1312157","labels":{"en":{"language":"en","value":"Experimenting with Isabelle in ZF set theory"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 488232"}},"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":"Q1312157$36A86F8F-3FF9-45B3-AB06-D56273153DAE","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"c654416857d0b9a6a8c34d9b063147a2995a8f99","datavalue":{"value":{"text":"Experimenting with Isabelle in ZF set theory","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q1312157$BBCAE1DB-685F-41A3-AC55-637FB69EF164","rank":"normal"}],"P225":[{"mainsnak":{"snaktype":"value","property":"P225","hash":"95ddfb2d50abaf35b9d746532f9e452d262c33d3","datavalue":{"value":"0783.68109","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1312157$63242372-F7F6-487F-8D5F-4D28F92DA919","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"b96be165d01d6ab4711a7b140164def98ce4ac43","datavalue":{"value":"10.1007/BF00881863","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1312157$42EC3C2A-8D6C-4B6C-B388-37F59F4AC78F","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"b55e4620c91bf18f02baf538bbf4095712412dff","datavalue":{"value":{"entity-type":"item","numeric-id":1312156,"id":"Q1312156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1312157$2BD0B9C0-C476-4547-9C34-091F25D0414D","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":"Q1312157$75C475BD-B190-40E7-8FAF-10C4DEE02193","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"68b724eb687dbe57c6756b615ba860966fd43d36","datavalue":{"value":{"time":"+1994-01-19T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q1312157$47E9094C-E08C-4FB7-992F-82DF6323EF88","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e6e7c2e9d67f9590a26e18c734f34db53ce5ec87","datavalue":{"value":"68T15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1312157$5BEF763B-DCF5-4A33-A4B5-B9CEB46CC2CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d76b54ca3ec41228d05d0d48b5373554ccc0dcb3","datavalue":{"value":"03E30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1312157$53052315-D16C-42D6-B88C-AC9E8D8A6116","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"511e945733fe444198932edbee4ccaee614e0cde","datavalue":{"value":"488232","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q1312157$425B66FE-D5D3-45BA-A674-902B61F455BA","rank":"normal"}],"P1450":[{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f7eefb2b1f5e1ddd95f5db204b23cfb4c53d0151","datavalue":{"value":"Isabelle","type":"string"},"datatype":"string"},"type":"statement","id":"Q1312157$B79EF937-7E74-472E-84AF-DCAB8C0E413B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"b36a4092864d39bf9c99c5936b3d1261e44b9950","datavalue":{"value":"set theory","type":"string"},"datatype":"string"},"type":"statement","id":"Q1312157$9463E744-57D5-4D8D-8F0B-B8462424C48E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1450","hash":"f8c7361aca491a9cc26be4ba2a7deaecfb6f1c80","datavalue":{"value":"backward proofs","type":"string"},"datatype":"string"},"type":"statement","id":"Q1312157$7128CB1E-6B04-450A-8834-83FE408BA977","rank":"normal"}],"P1463":[{"mainsnak":{"snaktype":"value","property":"P1463","hash":"bab752e9cf98240487eb3aae10666dc541b36d41","datavalue":{"value":{"entity-type":"item","numeric-id":43692,"id":"Q43692"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1312157$9521F1FC-F394-43BE-92BE-D15F4FC416D8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1463","hash":"1aec27d540e360c78ddad230e6e300ced62bdec3","datavalue":{"value":{"entity-type":"item","numeric-id":18433,"id":"Q18433"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1312157$C961CD26-F82F-4CC3-8CC8-3AC8A57B4225","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":"Q1312157$DD0A7E50-D3BB-49AF-B9D9-2F871D63C22F","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":"Q1312157$3B6719D1-2885-46BC-8CBE-A1EB95DFEE0B","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":"Q1312157$562C7C41-9660-4765-99E5-BF3CCAD3E805","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"2edbd4db20ecbcbb1c315d5320a38ebf3acfa299","datavalue":{"value":{"entity-type":"item","numeric-id":3992552,"id":"Q3992552"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1312157$BB73BDB3-D825-4CCC-B7C4-98F5C0402128","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"85b58e334bbf84629d414ca7d6688164e5524fe2","datavalue":{"value":{"entity-type":"item","numeric-id":4726218,"id":"Q4726218"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1312157$2A8240BB-24A0-4CE0-B3DC-95C71B7923E3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f46aebace2a25a127b5f8fa91e5c1e1d9e767403","datavalue":{"value":{"entity-type":"item","numeric-id":1097252,"id":"Q1097252"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1312157$2178D199-8178-4BCF-84DB-8692FBDD258D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"feecea33ae1f303ddaaebbb480759d5a134569c9","datavalue":{"value":{"entity-type":"item","numeric-id":792991,"id":"Q792991"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1312157$16B6CE83-A49A-4A42-8C96-A74C86B90137","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"b25a738f1ae81498c7ab556280d1bceb30630674","datavalue":{"value":{"entity-type":"item","numeric-id":4739887,"id":"Q4739887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1312157$0CB1F5BE-1947-4D86-B0F6-B834AD1F4485","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f23417d0146cdc8808662ea4f0b0496e878f3547","datavalue":{"value":{"entity-type":"item","numeric-id":4722037,"id":"Q4722037"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1312157$D4F259B6-41DF-49E3-A407-DC63A61E55CA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"777f1902a1127b94884ae1ddc89768860f054a6e","datavalue":{"value":{"entity-type":"item","numeric-id":3789060,"id":"Q3789060"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1312157$7FFDD787-D25B-43D7-B6FA-4BC413E939B8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"1404903fbb3450c69ae4b46e148487834232fe43","datavalue":{"value":{"entity-type":"item","numeric-id":1823013,"id":"Q1823013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1312157$412C8E2F-1106-42DC-A0D4-B984B1D3962D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6f03c1548cfd1f167c04900a9c91718e8b0cab75","datavalue":{"value":{"entity-type":"item","numeric-id":4342088,"id":"Q4342088"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q1312157$4C95A4AB-D241-444A-8D46-02DC4B1BCAD4","rank":"normal"}],"P1643":[{"mainsnak":{"snaktype":"value","property":"P1643","hash":"24fe603be126cf3667eea9dd66064ca9076cdc76","datavalue":{"value":{"entity-type":"item","numeric-id":1904402,"id":"Q1904402"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"6cdb6459b247922a3dd3240d471bc97795f1947c","datavalue":{"value":{"amount":"+0.8130449056625366","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":"Q1312157$523ABDD6-86E5-48F5-9EC5-2DAC1FDEE38B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"ef914c5d16ae991870856bd539a5283395a477b7","datavalue":{"value":{"entity-type":"item","numeric-id":3543647,"id":"Q3543647"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"a6f4e74187c00765666d80ba55745f8eb0f66cdf","datavalue":{"value":{"amount":"+0.8086890578269958","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":"Q1312157$F023A688-6515-4B83-BA80-E857252922BD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"de72a55ad8714891c24ede823c98f307f17fcba8","datavalue":{"value":{"entity-type":"item","numeric-id":1319386,"id":"Q1319386"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"49629c40c2551bc10fde5d5e03a3b65db06a2bf5","datavalue":{"value":{"amount":"+0.8085775971412659","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":"Q1312157$94BEDA11-1D55-4939-827D-3C8FEC3F5C99","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"1b18f1bcee5a559e76e86ee84dd5601244af54f6","datavalue":{"value":{"entity-type":"item","numeric-id":909488,"id":"Q909488"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"49629c40c2551bc10fde5d5e03a3b65db06a2bf5","datavalue":{"value":{"amount":"+0.8085775971412659","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":"Q1312157$1CA55F13-2F8B-40B3-BB47-2CC8BD8EC340","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1643","hash":"027e66e493294de396e3f06701b232a3660c5eaa","datavalue":{"value":{"entity-type":"item","numeric-id":1823013,"id":"Q1823013"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","qualifiers":{"P1659":[{"snaktype":"value","property":"P1659","hash":"57b7cc0106a26913a0eed7863665c8a1fe90a1bd","datavalue":{"value":{"amount":"+0.7750980257987976","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":"Q1312157$7E81B67C-E204-4563-B50B-3E1F4DFEA50B","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Experimenting with Isabelle in ZF set theory","badges":[]}}}}}