summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | eberlm <eberlm@in.tum.de> |

Tue, 20 Sep 2016 14:51:58 +0200 | |

changeset 63923 | c9bba9dba73b |

parent 63922 | d184a824aa63 |

child 63924 | f91766530e13 |

NEWS: Normalized_Fraction.thy

--- a/NEWS Tue Sep 20 11:35:10 2016 +0200 +++ b/NEWS Tue Sep 20 14:51:58 2016 +0200 @@ -276,6 +276,11 @@ * Theory Library/Perm.thy: basic facts about almost everywhere fix bijections. +* Theory Library/Normalized_Fraction.thy: allows viewing an element +of a field of fractions as a normalized fraction (i.e. a pair of +numerator and denominator such that the two are coprime and the +denominator is normalized w.r.t. unit factors) + * Locale bijection establishes convenient default simp rules like "inv f (f a) = a" for total bijections.