isabelle: src/Tools/Permanent_Interpretation.thy@31d810570879 (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
58889 5b7a9633cfa8 modernized header uniformly as section; wenzelm parents: 55601 diff changeset	5	section {* 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	wenzelm
	Thu, 29 Jan 2015 16:16:01 +0100
changeset 59470	31d810570879
parent 58889	5b7a9633cfa8
permissions	-rw-r--r--