isabelle: src/Tools/Permanent_Interpretation.thy@f620851148a9 (annotated)

55601 b7f4da504b75 offical tool haftmann parents: 55600 diff changeset	1	(* Title: Tools/Permanent_Interpretation.thy
b7f4da504b75 offical tool haftmann parents: 55600 diff changeset	2	Author: Florian Haftmann, TU Muenchen
41582 c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: diff changeset	3	*)
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: diff changeset	4
55601 b7f4da504b75 offical tool haftmann parents: 55600 diff changeset	5	header {* Permanent interpretation accompanied with mixin definitions. *}
41582 c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: diff changeset	6
55601 b7f4da504b75 offical tool haftmann parents: 55600 diff changeset	7	theory Permanent_Interpretation
41582 c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: diff changeset	8	imports Pure
55600 3c7610b8dcfc more convenient syntax for permanent interpretation haftmann parents: 55599 diff changeset	9	keywords "defining" and "permanent_interpretation" :: thy_goal
41582 c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: diff changeset	10	begin
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: diff changeset	11
55601 b7f4da504b75 offical tool haftmann parents: 55600 diff changeset	12	ML_file "~~/src/Tools/permanent_interpretation.ML"
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48644 diff changeset	13
41582 c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: diff changeset	14	end

author	desharna
	Thu, 14 Aug 2014 13:21:19 +0200
changeset 57933	f620851148a9
parent 55601	b7f4da504b75
child 58889	5b7a9633cfa8
permissions	-rw-r--r--