equal
deleted
inserted
replaced
5 header {* Embedding (a subset of) the Pure term algebra in HOL *} |
5 header {* Embedding (a subset of) the Pure term algebra in HOL *} |
6 |
6 |
7 theory CodeEmbed |
7 theory CodeEmbed |
8 imports Main MLString |
8 imports Main MLString |
9 begin |
9 begin |
10 |
|
11 section {* Embedding (a subset of) the Pure term algebra in HOL *} |
|
12 |
|
13 |
10 |
14 subsection {* Definitions *} |
11 subsection {* Definitions *} |
15 |
12 |
16 types vname = ml_string; |
13 types vname = ml_string; |
17 types "class" = ml_string; |
14 types "class" = ml_string; |