| changeset 63374 | 1a474286f315 |
| parent 63354 | 6038ba2687cf |
| child 63375 | 59803048b0e8 |
--- a/NEWS Mon Jul 04 19:46:19 2016 +0200 +++ b/NEWS Mon Jul 04 19:46:19 2016 +0200 @@ -136,6 +136,9 @@ *** HOL *** +* Locale bijection establishes convenient default simp rules +like "inv f (f a) = a" for total bijections. + * Former locale lifting_syntax is now a bundle, which is easier to include in a local context or theorem statement, e.g. "context includes lifting_syntax begin ... end". Minor INCOMPATIBILITY.