src/HOL/ex/Interpretation_with_Defs.thy
author hoelzl
Thu Jan 31 11:31:27 2013 +0100 (2013-01-31)
changeset 50999 3de230ed0547
parent 48891 c0eafbd55de3
child 55599 6535c537b243
permissions -rw-r--r--
introduce order topology
haftmann@41582
     1
(*  Title:      HOL/ex/Interpretation_with_Defs.thy
haftmann@41582
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@41582
     3
*)
haftmann@41582
     4
haftmann@41582
     5
header {* Interpretation accompanied with mixin definitions.  EXPERIMENTAL. *}
haftmann@41582
     6
haftmann@41582
     7
theory Interpretation_with_Defs
haftmann@41582
     8
imports Pure
haftmann@41582
     9
begin
haftmann@41582
    10
wenzelm@48891
    11
ML_file "~~/src/Tools/interpretation_with_defs.ML"
wenzelm@48891
    12
haftmann@41582
    13
end