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
     1 (*  Title:      HOL/ex/Interpretation_with_Defs.thy
     2     Author:     Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Interpretation accompanied with mixin definitions.  EXPERIMENTAL. *}
     6 
     7 theory Interpretation_with_Defs
     8 imports Pure
     9 begin
    10 
    11 ML_file "~~/src/Tools/interpretation_with_defs.ML"
    12 
    13 end