changeset 63377 | 64adf4ba9526 |
parent 63375 | 59803048b0e8 |
child 63378 | 161f3ce4bf45 |
--- a/NEWS Mon Jul 04 19:46:20 2016 +0200 +++ b/NEWS Mon Jul 04 19:46:20 2016 +0200 @@ -136,6 +136,9 @@ *** HOL *** +* Theory Library/Combinator_PER.thy: combinator to build partial +equivalence relations from a predicate and an equivalenc relation. + * Theory Library/Perm.thy: basic facts about almost everywhere fix bijections.