equal
deleted
inserted
replaced
273 * Theory Library/Combinator_PER.thy: combinator to build partial |
273 * Theory Library/Combinator_PER.thy: combinator to build partial |
274 equivalence relations from a predicate and an equivalence relation. |
274 equivalence relations from a predicate and an equivalence relation. |
275 |
275 |
276 * Theory Library/Perm.thy: basic facts about almost everywhere fix |
276 * Theory Library/Perm.thy: basic facts about almost everywhere fix |
277 bijections. |
277 bijections. |
|
278 |
|
279 * Theory Library/Normalized_Fraction.thy: allows viewing an element |
|
280 of a field of fractions as a normalized fraction (i.e. a pair of |
|
281 numerator and denominator such that the two are coprime and the |
|
282 denominator is normalized w.r.t. unit factors) |
278 |
283 |
279 * Locale bijection establishes convenient default simp rules |
284 * Locale bijection establishes convenient default simp rules |
280 like "inv f (f a) = a" for total bijections. |
285 like "inv f (f a) = a" for total bijections. |
281 |
286 |
282 * Former locale lifting_syntax is now a bundle, which is easier to |
287 * Former locale lifting_syntax is now a bundle, which is easier to |