| changeset 1580 | 0faec4f7d737 |
| parent 1576 | 7b8f570b2450 |
| child 1595 | aeed597d2043 |
| 1579:5b0bdd64956e | 1580:0faec4f7d737 |
|---|---|
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 |
6 |
7 ML {* val _ = cheat_fv_rsp := false *} |
|
8 ML {* val _ = cheat_alpha_bn_rsp := false *} |
|
9 ML {* val _ = cheat_equivp := false *} |
7 ML {* val _ = cheat_equivp := false *} |
10 |
8 |
11 nominal_datatype t = |
9 nominal_datatype t = |
12 Var "name" |
10 Var "name" |
13 | Fun "t" "t" |
11 | Fun "t" "t" |