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 declare [[STEPS = 14]] |
7 declare [[STEPS = 15]] |
8 |
8 |
9 nominal_datatype trm = |
9 nominal_datatype trm = |
10 Var "name" |
10 Var "name" |
11 | App "trm" "trm" |
11 | App "trm" "trm" |
12 | Lam x::"name" t::"trm" bind_set x in t |
12 | Lam x::"name" t::"trm" bind_set x in t |
13 | Let a::"assg" t::"trm" bind_set "bn a" in t |
13 | Let a::"assg" t::"trm" bind_set "bn a" in t |
14 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind_set x in y t t1 t2 |
14 | Foo x::"name" y::"name" t::"trm" t1::"trm" t2::"trm" bind_set x in y t t1 t2 |
18 As "name" x::"name" t::"trm" bind x in t |
18 As "name" x::"name" t::"trm" bind x in t |
19 binder |
19 binder |
20 bn::"assg \<Rightarrow> atom set" |
20 bn::"assg \<Rightarrow> atom set" |
21 where |
21 where |
22 "bn (As x y t) = {atom x}" |
22 "bn (As x y t) = {atom x}" |
|
23 |
|
24 typ trm |
|
25 typ assg |
23 |
26 |
24 thm trm_assg.fv |
27 thm trm_assg.fv |
25 thm trm_assg.supp |
28 thm trm_assg.supp |
26 thm trm_assg.eq_iff |
29 thm trm_assg.eq_iff |
27 thm trm_assg.bn |
30 thm trm_assg.bn |