isabelle: src/HOL/ex/Interpretation_with_Defs.thy@6535c537b243 (annotated)

41582 c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: diff changeset	1	(* Title: HOL/ex/Interpretation_with_Defs.thy
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: diff changeset	2	Author: Florian Haftmann, TU Muenchen
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
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: diff changeset	5	header {* Interpretation accompanied with mixin definitions. EXPERIMENTAL. *}
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: diff changeset	6
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: diff changeset	7	theory Interpretation_with_Defs
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example haftmann parents: diff changeset	8	imports Pure
55599 6535c537b243 aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation" haftmann parents: 48891 diff changeset	9	keywords "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
48891 c0eafbd55de3 prefer ML_file over old uses; wenzelm parents: 48644 diff changeset	12	ML_file "~~/src/Tools/interpretation_with_defs.ML"
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	haftmann
	Wed, 19 Feb 2014 22:05:05 +0100
changeset 55599	6535c537b243
parent 48891	c0eafbd55de3
child 55600	3c7610b8dcfc
permissions	-rw-r--r--