{"entities":{"Q7361547":{"pageid":31520180,"ns":120,"title":"Item:Q7361547","lastrevid":105368216,"modified":"2026-10-07T13:37:21Z","type":"item","id":"Q7361547","labels":{"en":{"language":"en","value":"AutoCorres2"}},"descriptions":{"en":{"language":"en","value":"AFP entry AutoCorres2"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"333b5ad1f078760ad60793bd3f15a9a97b5f4cfd","datavalue":{"value":"https://isa-afp.org/entries/AutoCorres2.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361547$F0D40806-5101-4BC0-9F17-E9E9A3512C91","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"0d62637b15884a61f1d72563c2b82e242295c57a","datavalue":{"value":{"time":"+2024-04-17T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361547$A07BA8B0-5143-4ED4-A952-7187F1030E08","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"a3e83d0f24560a652509bafb50beccfa178b2d30","datavalue":{"value":"Matthew Brecknell","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361547$8F9673A0-FC22-487A-B954-D7B698B3D5D6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"57e4aa39545daad2fe8f664a49d9ae9bb96ad1e9","datavalue":{"value":"David Greenaway","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361547$634972C2-C702-4F64-86B0-690933500470","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"01b202f25e5390ba0104cc409e25272c5fbddba4","datavalue":{"value":"Johannes H\u00f6lzl","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361547$9B96317F-F898-4A7F-8965-920E7C9509CD","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"283f1bfcca6dad06181e4c5e3bf9d823639da8ad","datavalue":{"value":"Fabian Immler","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361547$70D6C3A8-F451-4A39-8EB9-FF11E7C9AE75","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"46145f92c416e0014f5972c8ef4f728e7419b9b2","datavalue":{"value":"Gerwin Klein","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361547$FD8C59CC-9FC4-4EDB-9FC3-D418E01F1888","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"9fa6183578d80badfa7cba05e2fcf62073b3650f","datavalue":{"value":"Rafal Kolanski","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361547$9652EB71-FED5-488C-81C3-E15CBAB67342","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"3be41d58a3dc42bd83bedffcd1f5904218b2ab86","datavalue":{"value":"Japheth Lim","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361547$F9CA36D9-D5FF-416E-9BB6-53BBCADA7666","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"f8537166c3530c582210a124f9867c7c25c26ffe","datavalue":{"value":"Michael Norrish","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361547$F9CB661E-A7A6-41BF-958A-4BDCE0BBAD05","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"45e860162f4b3c0ff9ec8446d8b1743804a3a1b4","datavalue":{"value":"Norbert Schirmer","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361547$B4378018-5B43-465F-BAE6-86D0E390C403","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"34ca23e13f3744b21ae1779c590b97468a47c009","datavalue":{"value":"Salomon Sickert","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361547$65351E6E-5D78-454A-B7E5-8759D7197090","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"4c15075fe9cbdbb8435df15e8ff3758cb0689396","datavalue":{"value":"Thomas Sewell","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361547$E1335E21-71B7-4751-9F54-C5514059EFF6","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"5cd39b3f12a134fb2ab6e29d4c5408ce90801994","datavalue":{"value":"Harvey Tuch","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361547$9BF3F4AB-7F46-4CFD-BC93-EB399A84350E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"8ad3851178fd4351b5225d703448b2fe1218d392","datavalue":{"value":"Simon Wimmer","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361547$97789C01-0CF6-4F3C-B959-A66462C7483A","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"8245c763f50138edbd19277cc1f6637ff7541768","datavalue":{"value":{"text":"AutoCorres2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361547$DD1D910D-7023-47CF-B54F-5C35256F57E4","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"2cc1669c40e4c5a8e5d0ba65cee8011deea07c37","datavalue":{"value":"AutoCorres2 is a tool to facilitate the verification of C programs within Isabelle. It is a fork of AutoCorres .","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361547$C8E03E0F-8F9C-4AEF-92A3-3A5FC4AFCE9D","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"0cb6a694c413940271a785e87645155d12c05123","datavalue":{"value":{"entity-type":"item","numeric-id":2914735,"id":"Q2914735"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361547$C092C891-3096-4E61-953E-7D22593717C0","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":"Q7361547$9898D9F2-7EDA-4017-BF8F-3B8092C1A010","rank":"normal"}],"P37":[{"mainsnak":{"snaktype":"value","property":"P37","hash":"9a21a8eebe97539644aa32b24dda137c12e751dc","datavalue":{"value":{"entity-type":"item","numeric-id":40327,"id":"Q40327"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361547$E462E06F-7468-49AF-A8CC-4F12988485AB","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"282e516eeb9a5d288cbb79982845ccda1806c806","datavalue":{"value":{"entity-type":"item","numeric-id":7361671,"id":"Q7361671"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361547$55F31E13-0AFF-4991-B794-33CDD1F868BC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"e63516e58241acf42ac71681fd6610456ac84f3f","datavalue":{"value":{"entity-type":"item","numeric-id":7361376,"id":"Q7361376"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361547$9D53EC7D-3151-4B5B-964F-B16B42FDC441","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"aa8f6bd5a2b4440f838b34acf103bdf45fee4f56","datavalue":{"value":{"entity-type":"item","numeric-id":7360797,"id":"Q7360797"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361547$13D4B434-BA90-4739-BBDA-B6C2E8003C46","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"7a918ca57cbef7417c708001c9499e7e295238c0","datavalue":{"value":{"entity-type":"item","numeric-id":7360836,"id":"Q7360836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361547$71B07C8C-4D3C-4786-8EBF-8F3B2B17201D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P2651","hash":"9beb5f7be6b27e22c4af581585b828086bbf7950","datavalue":{"value":{"entity-type":"item","numeric-id":7360796,"id":"Q7360796"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361547$BC9FF731-D0C6-4A06-89BE-DD7E95D827A8","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":"Q7361547$F78584E4-995F-4815-9E8C-9CD959CDD43F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"AutoCorres2","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/AutoCorres2"}}}}}