NEWS
changeset 30305 720226bedc4d
parent 30273 ecd6f0ca62ea
parent 30304 d8e4cd2ac2a1
child 30308 23935abfb549
equal deleted inserted replaced
30274:44832d503659 30305:720226bedc4d
   217 demanding keyword 'by' and supporting the full method expression
   217 demanding keyword 'by' and supporting the full method expression
   218 syntax just like the Isar command 'by'.
   218 syntax just like the Isar command 'by'.
   219 
   219 
   220 
   220 
   221 *** HOL ***
   221 *** HOL ***
       
   222 
       
   223 * Some set operations are now proper qualified constants with authentic syntax.
       
   224 INCOMPATIBILITY:
       
   225 
       
   226     op Int ~>   Set.Int
       
   227     op Un ~>    Set.Un
       
   228     INTER ~>    Set.INTER
       
   229     UNION ~>    Set.UNION
       
   230     Inter ~>    Set.Inter
       
   231     Union ~>    Set.Union
       
   232     {} ~>       Set.empty
       
   233     UNIV ~>     Set.UNIV
       
   234 
       
   235 * Class complete_lattice with operations Inf, Sup, INFI, SUPR now in theory
       
   236 Set.
   222 
   237 
   223 * Auxiliary class "itself" has disappeared -- classes without any parameter
   238 * Auxiliary class "itself" has disappeared -- classes without any parameter
   224 are treated as expected by the 'class' command.
   239 are treated as expected by the 'class' command.
   225 
   240 
   226 * Leibnitz's Series for Pi and the arcus tangens and logarithm series.
   241 * Leibnitz's Series for Pi and the arcus tangens and logarithm series.
   295 * If methods "eval" and "evaluation" encounter a structured proof state
   310 * If methods "eval" and "evaluation" encounter a structured proof state
   296 with !!/==>, only the conclusion is evaluated to True (if possible),
   311 with !!/==>, only the conclusion is evaluated to True (if possible),
   297 avoiding strange error messages.
   312 avoiding strange error messages.
   298 
   313 
   299 * Simplifier: simproc for let expressions now unfolds if bound variable
   314 * Simplifier: simproc for let expressions now unfolds if bound variable
   300 occurs at most one time in let expression body.  INCOMPATIBILITY.
   315 occurs at most once in let expression body.  INCOMPATIBILITY.
   301 
   316 
   302 * New classes "top" and "bot" with corresponding operations "top" and "bot"
   317 * New classes "top" and "bot" with corresponding operations "top" and "bot"
   303 in theory Orderings;  instantiation of class "complete_lattice" requires
   318 in theory Orderings;  instantiation of class "complete_lattice" requires
   304 instantiation of classes "top" and "bot".  INCOMPATIBILITY.
   319 instantiation of classes "top" and "bot".  INCOMPATIBILITY.
   305 
   320