src/Tools/Permanent_Interpretation.thy
author haftmann
Sun Sep 21 16:56:11 2014 +0200 (2014-09-21)
changeset 58410 6d46ad54a2ab
parent 55601 b7f4da504b75
child 58889 5b7a9633cfa8
permissions -rw-r--r--
explicit separation of signed and unsigned numerals using existing lexical categories num and xnum
     1 (*  Title:   Tools/Permanent_Interpretation.thy
     2     Author:  Florian Haftmann, TU Muenchen
     3 *)
     4 
     5 header {* Permanent interpretation accompanied with mixin definitions. *}
     6 
     7 theory Permanent_Interpretation
     8 imports Pure
     9 keywords "defining" and "permanent_interpretation" :: thy_goal
    10 begin
    11 
    12 ML_file "~~/src/Tools/permanent_interpretation.ML"
    13 
    14 end