| changeset 2603 | 90779aefbf1a |
| parent 2602 | bcf558c445a4 |
| child 2607 | 7430e07a5d61 |
| 2602:bcf558c445a4 | 2603:90779aefbf1a |
|---|---|
21 binder |
21 binder |
22 bn::"assg \<Rightarrow> atom list" |
22 bn::"assg \<Rightarrow> atom list" |
23 where |
23 where |
24 "bn (As x y t a) = [atom x] @ bn a" |
24 "bn (As x y t a) = [atom x] @ bn a" |
25 | "bn (As_Nil) = []" |
25 | "bn (As_Nil) = []" |
26 |
|
27 term "bn" |
|
28 |
|
29 |
|
26 |
30 |
27 thm foo.bn_defs |
31 thm foo.bn_defs |
28 thm foo.permute_bn |
32 thm foo.permute_bn |
29 thm foo.perm_bn_alpha |
33 thm foo.perm_bn_alpha |
30 thm foo.perm_bn_simps |
34 thm foo.perm_bn_simps |