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 quotient_definition |
|
46 "permute_bn1 :: perm \<Rightarrow> assg \<Rightarrow> assg" |
|
47 is |
|
48 "permute_bn1_raw" |
|
49 |
|
50 quotient_definition |
|
51 "permute_bn2 :: perm \<Rightarrow> assg \<Rightarrow> assg" |
|
52 is |
|
53 "permute_bn2_raw" |
|
54 |
|
55 quotient_definition |
|
56 "permute_bn3 :: perm \<Rightarrow> assg \<Rightarrow> assg" |
|
57 is |
|
58 "permute_bn3_raw" |
|
59 |
45 |
60 lemmas permute_bn1 = permute_bn1_raw.simps[quot_lifted] |
46 lemmas permute_bn1 = permute_bn1_raw.simps[quot_lifted] |
61 lemmas permute_bn2 = permute_bn2_raw.simps[quot_lifted] |
47 lemmas permute_bn2 = permute_bn2_raw.simps[quot_lifted] |
62 lemmas permute_bn3 = permute_bn3_raw.simps[quot_lifted] |
48 lemmas permute_bn3 = permute_bn3_raw.simps[quot_lifted] |
63 |
49 |