equal
deleted
inserted
replaced
2 imports "../NewParser" |
2 imports "../NewParser" |
3 begin |
3 begin |
4 |
4 |
5 atom_decl name |
5 atom_decl name |
6 |
6 |
7 ML {* Function.add_function *} |
|
8 |
|
9 ML {* print_depth 50 *} |
|
10 declare [[STEPS = 9]] |
7 declare [[STEPS = 9]] |
11 |
8 |
12 |
9 |
13 nominal_datatype trm = |
10 nominal_datatype trm = |
14 Var "name" |
11 Var "name" |
16 | Lam x::"name" t::"trm" bind_set x in t |
13 | Lam x::"name" t::"trm" bind_set x in t |
17 | Let a::"assg" t::"trm" bind_set "bn a" in t |
14 | Let a::"assg" t::"trm" bind_set "bn a" in t |
18 | Foo x::"name" y::"name" t::"trm" bind_set x in y t |
15 | Foo x::"name" y::"name" t::"trm" bind_set x in y t |
19 | Bar x::"name" y::"name" t::"trm" bind y x in t x y |
16 | Bar x::"name" y::"name" t::"trm" bind y x in t x y |
20 and assg = |
17 and assg = |
21 As "name" "trm" |
18 As "name" "name" "trm" "name" |
22 binder |
19 binder |
23 bn::"assg \<Rightarrow> atom set" |
20 bn::"assg \<Rightarrow> atom set" |
24 where |
21 where |
25 "bn (As x t) = {atom x}" |
22 "bn (As x y t z) = {atom x}" |
26 |
23 |
27 ML {* Inductive.the_inductive *} |
24 ML {* Inductive.the_inductive *} |
28 thm trm_assg.fv |
25 thm trm_assg.fv |
29 thm trm_assg.supp |
26 thm trm_assg.supp |
30 thm trm_assg.eq_iff |
27 thm trm_assg.eq_iff |