{"entities":{"Q7361006":{"pageid":31518557,"ns":120,"title":"Item:Q7361006","lastrevid":105362381,"modified":"2026-10-07T13:34:12Z","type":"item","id":"Q7361006","labels":{"en":{"language":"en","value":"Nominal 2"}},"descriptions":{"en":{"language":"en","value":"AFP entry Nominal2"}},"aliases":{},"claims":{"P205":[{"mainsnak":{"snaktype":"value","property":"P205","hash":"504cbbf3ad90cbc75a76258e0e07eba664f8cfdc","datavalue":{"value":"https://isa-afp.org/entries/Nominal2.html","type":"string"},"datatype":"url"},"type":"statement","id":"Q7361006$A4238B33-AE8F-49F2-8EE1-35DF2CF84D4A","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"4ec88787b088b88fbcbfef6eb4534917e7df1ffe","datavalue":{"value":{"time":"+2013-02-21T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q7361006$098B9A1B-2DE1-4F52-88B7-A457D2D2BD4D","rank":"normal"}],"P43":[{"mainsnak":{"snaktype":"value","property":"P43","hash":"7538833d135040c28ea592b4b5e0506b7d8dd0b4","datavalue":{"value":"Christian Urban","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361006$D064DABF-C85B-4142-9C70-02A501D1CC54","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"42cc17b6ebd1e6b2e2779d5c2e7eb07525a54975","datavalue":{"value":"Stefan Berghofer","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361006$D04768A1-4BBB-46E9-9C04-E2238A4990B1","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P43","hash":"24ecedfcd986881afa2237d024b26ac8d56865f3","datavalue":{"value":"Cezary Kaliszyk","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361006$5A6DDAD5-4737-4548-92CF-C296716FE166","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"b01acc03bb891c0600546d4a9154769346587c80","datavalue":{"value":{"text":"Nominal 2","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q7361006$C4441D2F-0F2A-41E4-8AD0-E4185B659530","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"a76684a4c743ec184eece599fd9ca9e969841515","datavalue":{"value":"Dealing with binders, renaming of bound variables, capture-avoiding substitution, etc., is very often a major problem in formal proofs, especially in proofs by structural and rule induction. Nominal Isabelle is designed to make such proofs easy to formalise: it provides an infrastructure for declaring nominal datatypes (that is alpha-equivalence classes) and for defining functions over them by structural recursion. It also provides induction principles that have Barendregt\u2019s variable convention already built in. This entry can be used as a more advanced replacement for HOL/Nominal in the Isabelle distribution.","type":"string"},"datatype":"string"},"type":"statement","id":"Q7361006$EBFC2C03-0C8E-4DF9-A58F-9C803336E9A8","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":"Q7361006$F2CF84D5-C5E7-4AE9-968A-37B0575FAA80","rank":"normal"}],"P585":[{"mainsnak":{"snaktype":"value","property":"P585","hash":"c6381c3139ee5dae1881d28867a7925513419337","datavalue":{"value":{"entity-type":"item","numeric-id":7361667,"id":"Q7361667"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q7361006$C3018270-2EBF-43A3-AB29-1AA673C1E03B","rank":"normal"}],"P2651":[{"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":"Q7361006$72B7525E-BB7B-489B-8F6D-7A598D79737A","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":"Q7361006$D59AEDD2-DA91-432E-9F1E-9B8208E05E5F","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Nominal 2","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Nominal_2"}}}}}