equal
deleted
inserted
replaced
40 thm foo.supports |
40 thm foo.supports |
41 thm foo.fsupp |
41 thm foo.fsupp |
42 thm foo.supp |
42 thm foo.supp |
43 thm foo.fresh |
43 thm foo.fresh |
44 |
44 |
45 primrec |
|
46 permute_bn1_raw |
|
47 where |
|
48 "permute_bn1_raw p (As_raw x y t) = As_raw (p \<bullet> x) y t" |
|
49 |
|
50 primrec |
|
51 permute_bn2_raw |
|
52 where |
|
53 "permute_bn2_raw p (As_raw x y t) = As_raw x (p \<bullet> y) t" |
|
54 |
|
55 primrec |
|
56 permute_bn3_raw |
|
57 where |
|
58 "permute_bn3_raw p (As_raw x y t) = As_raw (p \<bullet> x) (p \<bullet> y) t" |
|
59 |
|
60 quotient_definition |
45 quotient_definition |
61 "permute_bn1 :: perm \<Rightarrow> assg \<Rightarrow> assg" |
46 "permute_bn1 :: perm \<Rightarrow> assg \<Rightarrow> assg" |
62 is |
47 is |
63 "permute_bn1_raw" |
48 "permute_bn1_raw" |
64 |
49 |