| changeset 66451 | 5be0b0604d71 |
| parent 66450 | a8299195ed82 |
| child 66455 | 158c513a39f5 |
--- a/NEWS Thu Aug 17 22:29:30 2017 +0200 +++ b/NEWS Fri Aug 18 14:57:23 2017 +0200 @@ -121,6 +121,9 @@ *** HOL *** +* Theory Library/Pattern_Aliases provides input syntax for pattern +aliases as known from Haskell, Scala and ML. + * Constant "subseq" in Topological_Spaces removed and subsumed by "strict_mono". Some basic lemmas specific to "subseq" have been renamed accordingly, e.g. "subseq_o" -> "strict_mono_o" etc.