{"entities":{"Q14275":{"pageid":14331,"ns":120,"title":"Item:Q14275","lastrevid":56564028,"modified":"2026-03-13T11:06:57Z","type":"item","id":"Q14275","labels":{"en":{"language":"en","value":"Isabelle/HOL"}},"descriptions":{},"aliases":{},"claims":{"P13":[{"mainsnak":{"snaktype":"value","property":"P13","hash":"0fee7f32ea7f4a28831996552522a43db0bf6f52","datavalue":{"value":"1569","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$E8C98BBA-DD02-4514-8E20-339256F540E1","rank":"normal"}],"P286":[{"mainsnak":{"snaktype":"value","property":"P286","hash":"cddf688eef7677022b9d2887abb2b66e0f4bf8b7","datavalue":{"value":{"entity-type":"item","numeric-id":4246952,"id":"Q4246952"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$92A4C810-7066-409A-A372-D414053F3F98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P286","hash":"b593934100b8367d353e2c491a3dd7049ac40083","datavalue":{"value":{"entity-type":"item","numeric-id":3172879,"id":"Q3172879"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$0D37C3F5-0C70-4934-9010-858E3A881755","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"908c3454b3659c4b140ccce33c5aee31081edc8d","datavalue":{"value":{"entity-type":"item","numeric-id":5976450,"id":"Q5976450"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$B8426F5B-A107-4C04-9E9C-8E9DF12E7B65","rank":"normal"}],"P29":[{"mainsnak":{"snaktype":"value","property":"P29","hash":"2a214521b9d6cc46681a6c82bbe3e996416b7b8c","datavalue":{"value":"http://www.cl.cam.ac.uk/research/hvg/Isabelle/","type":"string"},"datatype":"url"},"type":"statement","id":"Q14275$5C49F846-8287-42E1-A779-B1E99B503349","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"0db99c3b17fc587dc6d0b047e5ff5ce0de1786ab","datavalue":{"value":"03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$00554A28-2AF9-4327-99CE-C534E1D20E98","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"95bde9084e6ca63a8492631a417b047b22c72453","datavalue":{"value":"05","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$6E1DB554-C0B4-439B-9914-2F477ADE7D6B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fd3cd3c8cd085ac2048034c2279872658062342d","datavalue":{"value":"11","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$9B517091-A85B-4680-9F99-09B54E3D1DA3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"acf10290b955a69659a681d98822944f91bbad9e","datavalue":{"value":"68","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$B27560E9-E5AA-44C2-BB5A-481179198883","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"bebb7aa66b6973aa3a0c9749da8f6cd6626bb594","datavalue":{"value":"94","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$BDB5EB19-E9A1-4ABD-B65C-E3C3ECD8DB70","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ae9c75c1f07ce06d85b9552d2104619090f82402","datavalue":{"value":"00","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$4220332B-6F91-4044-8884-B7CA67287F9A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ccc624529bfb589cae1d19db3eb04dd4b43978c3","datavalue":{"value":"01","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$D25301A7-4833-4CCB-9C3A-C43509A0C02A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d379e93a1cc3ab3df2a5b8d85c84eb0620f6469c","datavalue":{"value":"06","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$A41E3731-CB27-4ED0-8E4A-69EEBE8FC195","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d57514d4788d5abbd1056aadd506bc3f1b86263e","datavalue":{"value":"08","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$D9C337EE-5EED-454D-B1BB-0F155D1D44AF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5f5c899803a3ce2dc0dd1263cc65df28aab94054","datavalue":{"value":"12","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$6946E15A-5B20-4721-B01F-DB19E138554F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8befc1ffe367aef867e4dcd902eb59cbacd3a347","datavalue":{"value":"13","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$88115461-7A5E-4CE7-B482-752139A4C464","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cd4f0694ac7a00e4fadde328cdb4437f6c066de7","datavalue":{"value":"14","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$E3935E5F-90E5-4CE6-A0B7-30CF08BB0D7C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5dd818343d7a5b259737eac61518c19de74ecd35","datavalue":{"value":"15","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$7B6FC392-6344-4048-BABE-553C8A7E6478","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c6cc7c76b3cafafac08dd013fc5ce16db183bb48","datavalue":{"value":"16","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$50EB7E1E-7483-4110-B118-F245AAEB86E1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"5f50a93e1fa52c1f7a63c5e1d98864f256220e6f","datavalue":{"value":"18","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$CC7DF0E0-546A-4644-A646-35B9A6C5BAA6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c42d8309659ef226cd875765a3c9064bb7558782","datavalue":{"value":"20","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$C1B2FDA9-F002-4CFA-93D9-9A552F592435","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d3fc854b328c20f46440ca61d9e1a4ed6cfc55e8","datavalue":{"value":"22","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$D01CB3BB-AF05-48BA-9D42-989E7B23902D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"fdcc80d920f5e4d163108380bb0c7de24bca08b4","datavalue":{"value":"26","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$A344989D-BF34-4F1C-98FC-B873D9AFA8B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"be5267d4895a58dcc5cf7a7e416f12795fbbed35","datavalue":{"value":"28","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$69F80E5F-E8E8-42D9-9A42-573B835D0EBA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ec41e560e80ab9e1fe0c779a012b3e380525af3f","datavalue":{"value":"30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$D2BBA9BC-A558-4948-A9EC-9EE515447391","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"548cd6c7cff28cd8fda861211c4340790df54fa7","datavalue":{"value":"32","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$E692433E-DC39-40F6-B728-71CDB79AF96B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"2e33fec5b481f44b815f9ae45229505143d48ec4","datavalue":{"value":"33","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$D012CCB9-4A6B-4087-AD7C-079D2ECD3B5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"3caa64e9b44e0e6a95be04e9d18f7428dc349506","datavalue":{"value":"34","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$4660B6F6-0312-40D4-A61E-3F876DD03FD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"8e00b180d44759253e9628090c3cb2c51b1a6ee8","datavalue":{"value":"35","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$FEF10833-2649-4DA7-9AA3-B98B6E7FAF5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"01c8c566de1600f59b5f8122a428964fb913122a","datavalue":{"value":"37","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$F0BB682E-2480-4286-A0B8-16FC98C01AC4","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ca97ab6736a2cf36b4aa3171cbf7b0139773b03d","datavalue":{"value":"46","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$E9E79D9A-5A38-45A0-9858-F1AA6BDA3B39","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9c36f543604e3fdf981f5fb6ed78b53d6c52253c","datavalue":{"value":"47","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$3D1084DD-FF6F-45C7-9348-61E2E6ECC918","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"be8e231fdb33dcfe6258f2f5ff03e1ecfad18bd7","datavalue":{"value":"49","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$3C029612-C5D6-4402-A16A-CC903E9E2520","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"389057ea232b6d266cab69038163241bd07104b6","datavalue":{"value":"51","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$DFC002C7-0B1B-40A0-BD14-85F66D01DD97","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"eb161afac2a132ba3ff878220cc5d73379a399b9","datavalue":{"value":"52","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$3C0818F9-D5DC-4717-A9BD-20DF71FEACEC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"43c1a4db523e8d5ed4d9f898b1f0303e17a6e259","datavalue":{"value":"53","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$3FCAB183-FAB2-46F2-A661-28083F19D467","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"85b50fc0bb13fa24d727c960e97501e2c7bce333","datavalue":{"value":"54","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$359DE655-50BC-47E0-91B0-950AAEDE22E8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"e24ee68b43931de13fa3c2edb783c4c41f7c841b","datavalue":{"value":"55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$F631C000-C0BA-4376-AB98-385A6C7546BA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cb0bb3315ea6d324166d2a3b9e8cc481541ca3cc","datavalue":{"value":"57","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$8EA2C08F-52BC-404F-B687-8DD9E5BBDA62","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a467a32e3049b1299c9c2b688461b7f273ec943","datavalue":{"value":"60","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$0162AB4F-8400-4159-90C2-4A7FE5F2CD48","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"a104733b1e30d91f56342777dc887a3edbb9e05f","datavalue":{"value":"65","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$5503F689-8095-467E-9BF2-5CD205C613C3","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"9cdce3acd819f327427a4823ff1d65533e6f5515","datavalue":{"value":"70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$5B295852-E2C6-468A-827E-03EE72CE00B6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"797ebe6b314441ca18070360b249a95d3ef9caa8","datavalue":{"value":"74","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$EBF2755D-8A03-46AC-BD9A-3FC2591FCAAC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"eafc2970861edb4c7004312b82ba31ab41f8cd06","datavalue":{"value":"76","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$972E50AC-E1C8-4911-9221-2D9629E746D1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"c596f9f2876e2dd8f650d5ff7592422666be753a","datavalue":{"value":"78","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$41D6B719-E938-4A78-89FE-90F06A54B1ED","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"4edc7e695c3667a3dc24594c0516548b87f81467","datavalue":{"value":"81","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$C96848BA-EF55-48C2-837A-917DB7E0BD86","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"70815976aa44d316576d629b9a9b2ae7fe77d360","datavalue":{"value":"83","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$BBED3129-4509-423D-868A-076CC89B3FD8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1ff47c21e9a366382fd12a5f20a4ed758079d385","datavalue":{"value":"86","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$B879F953-EFF7-49D6-A4CC-F88C5869180E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"541da1e359051dfcf3c498b9f1f1f8f905fbafe3","datavalue":{"value":"90","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$3C5450C2-63FD-4979-883E-B5573C070CBB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1a438efc028ac8f007fcfec586995516429ecdd8","datavalue":{"value":"91","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$34B46B5F-1745-44B4-8DD8-3F5165699BD7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"d0cfa49f62a5e301328cd7af9d04a50119944fd5","datavalue":{"value":"92","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$4107C6B7-2D52-4EB9-97F1-73F43B55688A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"7bfd76a3cee4b1dd54b082650152581ca2d695de","datavalue":{"value":"93","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$9D4A1105-E696-4A46-9BFE-885957E5181B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"cdd04b3c5243643f89ff1bab2287589642562be3","datavalue":{"value":"97","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q14275$EEA8E8E7-2463-42D4-913B-ABC9D892AB00","rank":"normal"}],"P1458":[{"mainsnak":{"snaktype":"value","property":"P1458","hash":"03281999c3208b8f3a62eaceadadf1ce834fe219","datavalue":{"value":{"entity-type":"item","numeric-id":12929,"id":"Q12929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$E1D75E9B-0742-4295-9DB2-96A0149D283F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ecda3e6d8e971c0b93d4cf3afb41990e853f830f","datavalue":{"value":{"entity-type":"item","numeric-id":13212,"id":"Q13212"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$7D0D8997-CC4A-42CE-A35A-E1746721D663","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"bb05cb23794774f62a8e4aa4de610af231973a1d","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$093E6DD7-094B-46A1-B6D8-9DC980B600FD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc41d9364226bfa8139f8dbc43b1b77967245f13","datavalue":{"value":{"entity-type":"item","numeric-id":17631,"id":"Q17631"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$92F9CE22-D383-45E3-8F76-EC802D059363","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"b82152c1528c5be7e2040d1abd74977f4fe51817","datavalue":{"value":{"entity-type":"item","numeric-id":18672,"id":"Q18672"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$990637DA-2479-4771-81B6-046FA4F999A5","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"331995fe532c23e24d72d01a1bd6245fafcd9671","datavalue":{"value":{"entity-type":"item","numeric-id":19106,"id":"Q19106"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$8610A663-50E8-42C9-A67C-9A199EAA9118","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cea2a7e9bb130921d12e1d361b3d4585036772c9","datavalue":{"value":{"entity-type":"item","numeric-id":16016,"id":"Q16016"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$63884B84-02CF-44F4-B8DE-500AD4A05B09","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2ded5a481ece08049848bd1edb3f9afa21f0df2f","datavalue":{"value":{"entity-type":"item","numeric-id":16873,"id":"Q16873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$C436DD7D-A53D-4D6D-9E4D-7FDF23D4FD0B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"cc4eff68b160f30b8d66dfcb610a0ea7a927079b","datavalue":{"value":{"entity-type":"item","numeric-id":17039,"id":"Q17039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$80668D23-BCEB-4F78-AEC1-CDA6A8F48539","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"ff80b41d03c65073c007c903a317be0a9c94293e","datavalue":{"value":{"entity-type":"item","numeric-id":13958,"id":"Q13958"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$D31003FE-4C61-4B24-9327-4CA46A295744","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"d6d29b9e294eea1a26ce05a4d8663847cfc55575","datavalue":{"value":{"entity-type":"item","numeric-id":16327,"id":"Q16327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$3BB7421A-5D53-49F5-97D6-DA0A0EEAB519","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"28fc316ccc1f38bd6830fcffe3187b6d32168084","datavalue":{"value":{"entity-type":"item","numeric-id":15455,"id":"Q15455"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$E987BEC8-0D9B-4491-95DD-BB7AFE5F8F3F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8533330b9fa0c1f7979d4af1d0e8bdba3ffc811c","datavalue":{"value":{"entity-type":"item","numeric-id":56651,"id":"Q56651"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$10B0E1B9-4980-47D0-8807-3A126D7B5071","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"8dde418bf28e22fefe1976bd953eb7c8ec5b548d","datavalue":{"value":{"entity-type":"item","numeric-id":16770,"id":"Q16770"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$BBE3AC6A-76A4-44B4-B439-EA6AD4475F33","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"139c69b2a23f419923a7989e28183ef8179b6836","datavalue":{"value":{"entity-type":"item","numeric-id":12833,"id":"Q12833"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$5EBADF2C-4FFF-47DB-AE24-D0ADDBC51ABF","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"acf5d0da134f7563af94342a3a34b9ca28cd59db","datavalue":{"value":{"entity-type":"item","numeric-id":23989,"id":"Q23989"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$05513A92-6223-4C66-A5D7-AF1DCA6C3F5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"7434bcf5c727d2c07e931aea1694436d0b39cd53","datavalue":{"value":{"entity-type":"item","numeric-id":27041,"id":"Q27041"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$548C9E5D-D197-444B-8030-8DCFF200C1C8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"85d5a2bfb7e5cd7e1dfb166523d6500a685410a1","datavalue":{"value":{"entity-type":"item","numeric-id":13377,"id":"Q13377"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$5B727B34-AA66-4560-82F5-BB7BA57254DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"144f0221487b5ba035abaca0f440960a9e47efeb","datavalue":{"value":{"entity-type":"item","numeric-id":27113,"id":"Q27113"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$DDF5187B-12E0-4FD2-A905-3B52B6804A2F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P1458","hash":"2fd4f2f31989858180fba533a04e1a60c8d16377","datavalue":{"value":{"entity-type":"item","numeric-id":22154,"id":"Q22154"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q14275$8475EBDD-A337-4A71-8521-9EC795740E75","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Isabelle/HOL","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Isabelle/HOL"}}}}}