equal
deleted
inserted
replaced
4 |
4 |
5 |
5 |
6 text {* example 3 or example 5 from Terms.thy *} |
6 text {* example 3 or example 5 from Terms.thy *} |
7 |
7 |
8 atom_decl name |
8 atom_decl name |
|
9 |
|
10 ML {* val _ = cheat_alpha_eqvt := true *} |
|
11 ML {* val _ = cheat_equivp := true *} |
9 |
12 |
10 nominal_datatype trm = |
13 nominal_datatype trm = |
11 Vr "name" |
14 Vr "name" |
12 | Ap "trm" "trm" |
15 | Ap "trm" "trm" |
13 | Lm x::"name" t::"trm" bind_set x in t |
16 | Lm x::"name" t::"trm" bind_set x in t |
27 thm trm_lts.perm |
30 thm trm_lts.perm |
28 thm trm_lts.induct |
31 thm trm_lts.induct |
29 thm trm_lts.distinct |
32 thm trm_lts.distinct |
30 thm trm_lts.supp |
33 thm trm_lts.supp |
31 thm trm_lts.fv[simplified trm_lts.supp] |
34 thm trm_lts.fv[simplified trm_lts.supp] |
|
35 |
|
36 declare permute_trm_raw_permute_lts_raw.simps[eqvt] |
|
37 declare alpha_gen_eqvt[eqvt] |
|
38 |
|
39 equivariance alpha_trm_raw |
32 |
40 |
33 (* why is this not in HOL simpset? *) |
41 (* why is this not in HOL simpset? *) |
34 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
42 lemma set_sub: "{a, b} - {b} = {a} - {b}" |
35 by auto |
43 by auto |
36 |
44 |