equal
deleted
inserted
replaced
167 comma separated list of theorem names rather than an ML expression; |
167 comma separated list of theorem names rather than an ML expression; |
168 |
168 |
169 * HOL/List: the constructors of type list are now Nil and Cons; |
169 * HOL/List: the constructors of type list are now Nil and Cons; |
170 INCOMPATIBILITY: while [] and infix # syntax is still there, of |
170 INCOMPATIBILITY: while [] and infix # syntax is still there, of |
171 course, ML tools referring to List.list.op # etc. have to be adapted; |
171 course, ML tools referring to List.list.op # etc. have to be adapted; |
172 |
|
173 |
172 |
174 |
173 |
175 *** LK *** |
174 *** LK *** |
176 |
175 |
177 * the notation <<...>> is now available as a notation for sequences of |
176 * the notation <<...>> is now available as a notation for sequences of |