src/HOL/Code_Evaluation.thy
changeset 50055 94041d602ecb
parent 48891 c0eafbd55de3
child 51112 da97167e03f7
equal deleted inserted replaced
50054:6da283e4497b 50055:94041d602ecb
     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 Predicate
     8 imports Plain Typerep New_DSequence
     9 begin
     9 begin
    10 
    10 
    11 subsection {* Term representation *}
    11 subsection {* Term representation *}
    12 
    12 
    13 subsubsection {* Terms and class @{text term_of} *}
    13 subsubsection {* Terms and class @{text term_of} *}