src/Tools/Permanent_Interpretation.thy
author blanchet
Mon, 15 Sep 2014 10:49:07 +0200
changeset 58335 a5a3b576fcfb
parent 55601 b7f4da504b75
child 58889 5b7a9633cfa8
permissions -rw-r--r--
generate 'code' attribute only if 'code' plugin is enabled
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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