equal
deleted
inserted
replaced
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 |
23 |
24 |
|
25 thm single_let.distinct |
24 thm single_let.distinct |
26 thm single_let.induct |
25 thm single_let.induct |
27 thm single_let.inducts |
26 thm single_let.inducts |
28 thm single_let.exhaust |
27 thm single_let.exhaust |
29 thm single_let.fv_defs |
28 thm single_let.fv_defs |
35 thm single_let.supports |
34 thm single_let.supports |
36 thm single_let.fsupp |
35 thm single_let.fsupp |
37 thm single_let.supp |
36 thm single_let.supp |
38 thm single_let.size |
37 thm single_let.size |
39 |
38 |
40 thm single_let.supp(1-2) |
|
41 thm single_let.fv_defs[simplified single_let.supp(1-2)] |
|
42 |
|
43 |
39 |
44 end |
40 end |
45 |
41 |
46 |
42 |
47 |
43 |