src/HOL/Code_Evaluation.thy
changeset 48891 c0eafbd55de3
parent 47108 2a1953f0d20d
child 50055 94041d602ecb
equal deleted inserted replaced
48890:d72ca5742f80 48891:c0eafbd55de3
     4 
     4 
     5 header {* Term evaluation using the generic code generator *}
     5 header {* Term evaluation using the generic code generator *}
     6 
     6 
     7 theory Code_Evaluation
     7 theory Code_Evaluation
     8 imports Plain Typerep Code_Numeral Predicate
     8 imports Plain Typerep Code_Numeral Predicate
     9 uses ("Tools/code_evaluation.ML")
       
    10 begin
     9 begin
    11 
    10 
    12 subsection {* Term representation *}
    11 subsection {* Term representation *}
    13 
    12 
    14 subsubsection {* Terms and class @{text term_of} *}
    13 subsubsection {* Terms and class @{text term_of} *}
    71 lemma eq_eq_TrueD:
    70 lemma eq_eq_TrueD:
    72   assumes "(x \<equiv> y) \<equiv> Trueprop True"
    71   assumes "(x \<equiv> y) \<equiv> Trueprop True"
    73   shows "x \<equiv> y"
    72   shows "x \<equiv> y"
    74   using assms by simp
    73   using assms by simp
    75 
    74 
    76 use "Tools/code_evaluation.ML"
    75 ML_file "Tools/code_evaluation.ML"
    77 
    76 
    78 code_reserved Eval Code_Evaluation
    77 code_reserved Eval Code_Evaluation
    79 
    78 
    80 setup {* Code_Evaluation.setup *}
    79 setup {* Code_Evaluation.setup *}
    81 
    80