equal
deleted
inserted
replaced
11 | App "trm" "trm" |
11 | App "trm" "trm" |
12 | Lam x::"name" t::"trm" bind x in t |
12 | Lam x::"name" t::"trm" bind x in t |
13 | Let a::"assg" t::"trm" bind "bn a" in t |
13 | Let a::"assg" t::"trm" bind "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 |
15 | Bar x::"name" y::"name" t::"trm" bind y x in t x y |
15 | Bar x::"name" y::"name" t::"trm" bind y x in t x y |
16 | Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (set) x in t2 |
16 | Baz x::"name" t1::"trm" t2::"trm" bind (set) x in t1, bind (res) x in t2 |
17 and assg = |
17 and assg = |
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 list" |
20 bn::"assg \<Rightarrow> atom list" |
21 where |
21 where |
22 "bn (As x y t) = [atom x]" |
22 "bn (As x y t) = [atom x]" |
|
23 |
|
24 |
23 |
25 |
24 thm single_let.distinct |
26 thm single_let.distinct |
25 thm single_let.induct |
27 thm single_let.induct |
26 thm single_let.inducts |
28 thm single_let.inducts |
27 thm single_let.exhaust |
29 thm single_let.exhaust |
32 thm single_let.fv_bn_eqvt |
34 thm single_let.fv_bn_eqvt |
33 thm single_let.size_eqvt |
35 thm single_let.size_eqvt |
34 thm single_let.supports |
36 thm single_let.supports |
35 thm single_let.fsupp |
37 thm single_let.fsupp |
36 thm single_let.supp |
38 thm single_let.supp |
37 thm single_let.size |
39 thm single_let.fresh |
38 |
40 |
39 |
41 |
40 end |
42 end |
41 |
43 |
42 |
44 |