equal
deleted
inserted
replaced
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 ML {* print_depth 50 *} |
7 ML {* print_depth 50 *} |
8 declare [[STEPS = 4]] |
8 declare [[STEPS = 5]] |
9 |
9 |
10 |
10 |
11 nominal_datatype trm = |
11 nominal_datatype trm = |
12 Var "name" |
12 Var "name" |
13 | App "trm" "trm" |
13 | App "trm" "trm" |
19 bn::"assg \<Rightarrow> atom set" |
19 bn::"assg \<Rightarrow> atom set" |
20 where |
20 where |
21 "bn (As x t) = {atom x}" |
21 "bn (As x t) = {atom x}" |
22 |
22 |
23 thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_raw.simps[no_vars] |
23 thm fv_trm_raw.simps[no_vars] fv_assg_raw.simps[no_vars] fv_bn_raw.simps[no_vars] bn_raw.simps[no_vars] |
|
24 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars] |
|
25 |
24 |
26 |
25 ML {* Inductive.the_inductive *} |
27 ML {* Inductive.the_inductive *} |
26 thm trm_assg.fv |
28 thm trm_assg.fv |
27 thm trm_assg.supp |
29 thm trm_assg.supp |
28 thm trm_assg.eq_iff |
30 thm trm_assg.eq_iff |