{"entities":{"Q7361232":{"pageid":31519235,"ns":120,"title":"Item:Q7361232","lastrevid":105364232,"modified":"2026-10-07T13:35:16Z","type":"item","id":"Q7361232","labels":{"en":{"language":"en","value":"Isabelle/DOF"}},"descriptions":{"en":{"language":"en","value":"AFP entry Isabelle_DOF"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"1d54db040a0ff1e8bf2389766e8b7012d752dfff","datavalue":{"value":"https://isa-afp.org/entries/Isabelle_DOF.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361232$0343AC1F-2B02-4156-B630-34AA48849AD7","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"227dbe0710d596965d91e536c510070ed1b54f65","datavalue":{"value":{"time":"+2024-04-26T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361232$FD70C5AA-3E7B-4DEE-A49D-C6D751479399","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"c321b6732f723699ff379c28a4499e7172aa303c","datavalue":{"value":"Achim D. Brucker","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361232$F708A70E-F494-4A5A-B49D-61FEE59040C2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"1349b1def488d035192a475ef478aa9bb97acc9b","datavalue":{"value":"Nicolas M\u00e9ric","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361232$1FF3E6A8-C384-43EE-936F-2294053E7042","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"9f417d50d28c3248f72294b3f5970214162e0fab","datavalue":{"value":"Burkhart Wolff","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361232$01313E35-B93D-4C53-A076-91A8B6EB2F6E","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"475054354d37b4ef3eab1a9ba36092e63476b789","datavalue":{"value":{"text":"Isabelle/DOF","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361232$7A8A9F73-A7A0-44A4-875C-04FC23AA97CD","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"5f9573603d4d0cb75447bffde17d640c4aa855e5","datavalue":{"value":"Isabelle/DOF provides an implementation of a document ontology framework on top of Isabelle/HOL. The framework allows both for defining ontologies and enforcing them during document development and document evolution. Isabelle/DOF targets use-cases such as mathematical texts referring to a theory development or technical reports requiring a particular structure. The documentation generation features are sufficiently powerful to typeset the most common cases without using LaTeX. Isabelle/DOF is integrated into Isabelle's IDE, which allows for smooth ontology development as well as immediate ontological conformance-checks during the editing of a document. Its checking facilities leverage the collaborative development of documents required to be consistent with an underlying ontological structure. This entry provides a user-manual with in-depth presentation of the design concepts of Isabelle/DOF's Ontology Definition Language (ODL) and describe comprehensively its major commands. Many examples show typical best-practice applications of the system.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361232$EE5C8BDC-91D1-453B-A7DC-229B1BE2889F","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9193dbfc7bccf141a4aab951ab2becf3c421ce66","datavalue":{"value":{"entity-type":"item","numeric-id":1126522,"id":"Q1126522"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361232$667985EF-F3CD-423C-BACC-844E1E00363F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"93d89c32c0d555889a53aec34946717c1964b8b5","datavalue":{"value":{"entity-type":"item","numeric-id":2843039,"id":"Q2843039"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361232$461C133A-4F86-417C-B519-5BB1F23B894D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3a46084cdd360a7e9420a94748dd7af52f87709a","datavalue":{"value":{"entity-type":"item","numeric-id":1798941,"id":"Q1798941"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361232$F902FCA9-DC14-43C0-B0C4-B498B9AE474F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"5bbf3fd853a4036d3cac2ccc1f0a3b4a11edb981","datavalue":{"value":{"entity-type":"item","numeric-id":2248021,"id":"Q2248021"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361232$50510714-0F5E-4587-B5FB-19B548548CAA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7affe87a5002ac44217cebc63f416898e488133c","datavalue":{"value":{"entity-type":"item","numeric-id":3750094,"id":"Q3750094"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361232$FDC32820-AC2F-45A3-8915-8E6C5028C72B","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":"Q7361232$BD7F5C46-A696-4A9A-B804-59A881E5924D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"8e97c3eb4cb2f11ca34697e2d3972f7b2b7bc1bc","datavalue":{"value":{"entity-type":"item","numeric-id":6487937,"id":"Q6487937"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361232$A916C873-1DAD-4489-8707-A621CD7F04F0","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"6a3f0c070d63cc8ade73e849526c8ff12c4b898b","datavalue":{"value":{"entity-type":"item","numeric-id":3523187,"id":"Q3523187"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361232$EA574AA1-C305-4C54-8144-CD971D5F3475","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"de630d14fe895ae5d892978d97f92afb82231aa0","datavalue":{"value":{"entity-type":"item","numeric-id":2879273,"id":"Q2879273"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361232$B93539C0-9371-49F3-8A69-92AB19B69B29","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":"Q7361232$FDA3C34F-DE63-4FDF-983C-BDA83A5E62E9","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"d34618100e140697fc3edbbe9a43a4c92fc8b2a9","datavalue":{"value":{"entity-type":"item","numeric-id":7361722,"id":"Q7361722"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361232$FBFCAAF7-C492-4492-9A2A-E1494A49E544","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P585","hash":"a0e462408f240420e2b3f4dd5e025dcac9e4a9cd","datavalue":{"value":{"entity-type":"item","numeric-id":7361044,"id":"Q7361044"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361232$338F90D2-1573-4E6A-8668-2B574F884E5F","rank":"normal"}],"P2651":[{"mainsnak":{"snaktype":"value","property":"P2651","hash":"65dbfb47d0b5da65bd2cdfbc8cab28721a9f7690","datavalue":{"value":{"entity-type":"item","numeric-id":7360803,"id":"Q7360803"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361232$467759A1-9DB0-4E4C-8128-058FCE998D9D","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":"Q7361232$47D6DD27-978F-4027-B2E9-629343DDCAEA","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Isabelle/DOF (AFP entry Isabelle DOF)","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Isabelle/DOF_(AFP_entry_Isabelle_DOF)"}}}}}