src/HOL/ex/Interpretation_with_Defs.thy
author nipkow
Fri, 21 Jun 2013 09:00:26 +0200
changeset 52402 c2f30ba4bb98
parent 48891 c0eafbd55de3
child 55599 6535c537b243
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
     9
begin
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    10
48891
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48644
diff changeset
    11
ML_file "~~/src/Tools/interpretation_with_defs.ML"
c0eafbd55de3 prefer ML_file over old uses;
wenzelm
parents: 48644
diff changeset
    12
41582
c34415351b6d experimental variant of interpretation with simultaneous definitions, plus example
haftmann
parents:
diff changeset
    13
end