equal
deleted
inserted
replaced
11 nominal_datatype trm = |
11 nominal_datatype trm = |
12 Var "name" |
12 Var "name" |
13 | App "trm" "trm" |
13 | App "trm" "trm" |
14 | Lam x::"name" t::"trm" bind_set x in t |
14 | Lam x::"name" t::"trm" bind_set x in t |
15 | Let a::"assg" t::"trm" bind_set "bn a" in t |
15 | Let a::"assg" t::"trm" bind_set "bn a" in t |
|
16 | Foo x::"name" y::"name" t::"trm" bind_set x in y t |
|
17 | Bar x::"name" y::"name" t::"trm" bind y x in t x y |
16 and assg = |
18 and assg = |
17 As "name" "trm" |
19 As "name" "trm" |
18 binder |
20 binder |
19 bn::"assg \<Rightarrow> atom set" |
21 bn::"assg \<Rightarrow> atom set" |
20 where |
22 where |
21 "bn (As x t) = {atom x}" |
23 "bn (As x t) = {atom x}" |
22 |
24 |
|
25 |
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] |
26 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] |
27 thm alpha_trm_raw_alpha_assg_raw_alpha_bn_raw.intros[no_vars] |
|
28 |
25 |
29 |
26 |
30 |
27 ML {* Inductive.the_inductive *} |
31 ML {* Inductive.the_inductive *} |
28 thm trm_assg.fv |
32 thm trm_assg.fv |
29 thm trm_assg.supp |
33 thm trm_assg.supp |