src/HOL/Code_Evaluation.thy
changeset 46664 1f6c140f9c72
parent 46638 fc315796794e
child 47108 2a1953f0d20d
equal deleted inserted replaced
46663:7fe029e818c2 46664:1f6c140f9c72
     3 *)
     3 *)
     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
     8 imports Plain Typerep Code_Numeral Predicate
     9 uses ("Tools/code_evaluation.ML")
     9 uses ("Tools/code_evaluation.ML")
    10 begin
    10 begin
    11 
    11 
    12 subsection {* Term representation *}
    12 subsection {* Term representation *}
    13 
    13