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 