| changeset 16417 | 9bc16273c2d4 |
| parent 14981 | e73f8140af78 |
| child 18461 | 9125d278fdc8 |
| 16416:6061ae1f90f2 | 16417:9bc16273c2d4 |
|---|---|
3 Author: Stefan Berghofer, TU Muenchen |
3 Author: Stefan Berghofer, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Terms over a given alphabet *} |
6 header {* Terms over a given alphabet *} |
7 |
7 |
8 theory Term = Main: |
8 theory Term imports Main begin |
9 |
9 |
10 datatype ('a, 'b) "term" = |
10 datatype ('a, 'b) "term" = |
11 Var 'a |
11 Var 'a |
12 | App 'b "('a, 'b) term list" |
12 | App 'b "('a, 'b) term list" |
13 |
13 |