equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 header {* Term evaluation using the generic code generator *} |
6 header {* Term evaluation using the generic code generator *} |
7 |
7 |
8 theory Code_Eval |
8 theory Code_Eval |
9 imports Plain "~~/src/HOL/Library/RType" |
9 imports Plain Typerep |
10 begin |
10 begin |
11 |
11 |
12 subsection {* Term representation *} |
12 subsection {* Term representation *} |
13 |
13 |
14 subsubsection {* Terms and class @{text term_of} *} |
14 subsubsection {* Terms and class @{text term_of} *} |