equal
deleted
inserted
replaced
118 history of serials allows to track potentially non-monotonous declarations |
118 history of serials allows to track potentially non-monotonous declarations |
119 appropriately. Minor INCOMPATIBILITY. |
119 appropriately. Minor INCOMPATIBILITY. |
120 |
120 |
121 |
121 |
122 *** HOL *** |
122 *** HOL *** |
|
123 |
|
124 * Theory Library/Pattern_Aliases provides input syntax for pattern |
|
125 aliases as known from Haskell, Scala and ML. |
123 |
126 |
124 * Constant "subseq" in Topological_Spaces removed and subsumed by |
127 * Constant "subseq" in Topological_Spaces removed and subsumed by |
125 "strict_mono". Some basic lemmas specific to "subseq" have been renamed |
128 "strict_mono". Some basic lemmas specific to "subseq" have been renamed |
126 accordingly, e.g. "subseq_o" -> "strict_mono_o" etc. |
129 accordingly, e.g. "subseq_o" -> "strict_mono_o" etc. |
127 |
130 |