equal
deleted
inserted
replaced
1 theory SingleLet |
1 theory SingleLet |
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
|
6 |
|
7 ML {* val _ = cheat_equivp := true *} |
6 |
8 |
7 nominal_datatype trm = |
9 nominal_datatype trm = |
8 Var "name" |
10 Var "name" |
9 | App "trm" "trm" |
11 | App "trm" "trm" |
10 | Lam x::"name" t::"trm" bind_set x in t |
12 | Lam x::"name" t::"trm" bind_set x in t |
25 thm trm_assg.perm |
27 thm trm_assg.perm |
26 thm trm_assg.induct |
28 thm trm_assg.induct |
27 thm trm_assg.inducts |
29 thm trm_assg.inducts |
28 thm trm_assg.distinct |
30 thm trm_assg.distinct |
29 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} |
31 ML {* Sign.of_sort @{theory} (@{typ trm}, @{sort fs}) *} |
30 thm trm_assg.fv[simplified trm_assg.supp(1-2)] |
32 (* thm trm_assg.fv[simplified trm_assg.supp(1-2)] *) |
31 |
33 |
32 |
34 |
33 end |
35 end |
34 |
36 |
35 |
37 |