equal
deleted
inserted
replaced
133 are generated into companion object of corresponding type class, to resolve |
133 are generated into companion object of corresponding type class, to resolve |
134 some situations where ambiguities may occur. |
134 some situations where ambiguities may occur. |
135 |
135 |
136 |
136 |
137 *** HOL *** |
137 *** HOL *** |
|
138 |
|
139 * Theory Library/Perm.thy: basic facts about almost everywhere fix |
|
140 bijections. |
138 |
141 |
139 * Locale bijection establishes convenient default simp rules |
142 * Locale bijection establishes convenient default simp rules |
140 like "inv f (f a) = a" for total bijections. |
143 like "inv f (f a) = a" for total bijections. |
141 |
144 |
142 * Former locale lifting_syntax is now a bundle, which is easier to |
145 * Former locale lifting_syntax is now a bundle, which is easier to |