equal
deleted
inserted
replaced
1 theory Ex1rec |
1 theory Ex1rec |
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
|
5 declare [[STEPS = 9]] |
|
6 |
5 atom_decl name |
7 atom_decl name |
6 |
|
7 ML {* val _ = cheat_supp_eq := true *} |
|
8 ML {* val _ = cheat_equivp := true *} |
|
9 |
8 |
10 nominal_datatype lam = |
9 nominal_datatype lam = |
11 Var "name" |
10 Var "name" |
12 | App "lam" "lam" |
11 | App "lam" "lam" |
13 | Lam x::"name" t::"lam" bind_set x in t |
12 | Lam x::"name" t::"lam" bind_set x in t |
16 Bp "name" "lam" |
15 Bp "name" "lam" |
17 binder |
16 binder |
18 bi::"bp \<Rightarrow> atom set" |
17 bi::"bp \<Rightarrow> atom set" |
19 where |
18 where |
20 "bi (Bp x t) = {atom x}" |
19 "bi (Bp x t) = {atom x}" |
|
20 |
|
21 |
|
22 thm alpha_lam_raw_alpha_bp_raw_alpha_bi_raw.intros |
21 |
23 |
22 thm lam_bp.fv |
24 thm lam_bp.fv |
23 thm lam_bp.eq_iff[no_vars] |
25 thm lam_bp.eq_iff[no_vars] |
24 thm lam_bp.bn |
26 thm lam_bp.bn |
25 thm lam_bp.perm |
27 thm lam_bp.perm |