| changeset 1595 | aeed597d2043 |
| parent 1576 | 7b8f570b2450 |
| child 1596 | c69d9fb16785 |
| 1594:892fcdb96c96 | 1595:aeed597d2043 |
|---|---|
1 theory TySch |
1 theory TySch |
2 imports "Parser" "../Attic/Prove" "FSet" |
2 imports "Parser" "../Attic/Prove" "FSet" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
|
7 ML {* val _ = cheat_equivp := false *} |
|
8 |
6 |
9 nominal_datatype t = |
7 nominal_datatype t = |
10 Var "name" |
8 Var "name" |
11 | Fun "t" "t" |
9 | Fun "t" "t" |
12 and tyS = |
10 and tyS = |