| changeset 63375 | 59803048b0e8 |
| parent 63374 | 1a474286f315 |
| child 63377 | 64adf4ba9526 |
--- a/NEWS Mon Jul 04 19:46:19 2016 +0200 +++ b/NEWS Mon Jul 04 19:46:20 2016 +0200 @@ -136,6 +136,9 @@ *** HOL *** +* Theory Library/Perm.thy: basic facts about almost everywhere fix +bijections. + * Locale bijection establishes convenient default simp rules like "inv f (f a) = a" for total bijections.