| changeset 25594 | 43c718438f9f |
| parent 25569 | c597835d5de4 |
| child 25603 | 4b7a58fc168c |
| 25593:0b0df6c8646a | 25594:43c718438f9f |
|---|---|
4 *) |
4 *) |
5 |
5 |
6 header {* A simple term evaluation mechanism *} |
6 header {* A simple term evaluation mechanism *} |
7 |
7 |
8 theory Eval |
8 theory Eval |
9 imports Main Pure_term |
9 imports PreList Pure_term |
10 begin |
10 begin |
11 |
11 |
12 subsection {* @{text typ_of} class *} |
12 subsection {* @{text typ_of} class *} |
13 |
13 |
14 class typ_of = |
14 class typ_of = |