equal
deleted
inserted
replaced
33 thm single_let.size_eqvt |
33 thm single_let.size_eqvt |
34 thm single_let.supports |
34 thm single_let.supports |
35 thm single_let.fsupp |
35 thm single_let.fsupp |
36 thm single_let.supp |
36 thm single_let.supp |
37 thm single_let.fresh |
37 thm single_let.fresh |
38 |
|
39 primrec |
|
40 permute_bn_raw |
|
41 where |
|
42 "permute_bn_raw p (As_raw x y t) = As_raw (p \<bullet> x) y t" |
|
43 |
38 |
44 quotient_definition |
39 quotient_definition |
45 "permute_bn :: perm \<Rightarrow> assg \<Rightarrow> assg" |
40 "permute_bn :: perm \<Rightarrow> assg \<Rightarrow> assg" |
46 is |
41 is |
47 "permute_bn_raw" |
42 "permute_bn_raw" |