NEWS
changeset 30298 abefe1dfadbb
parent 30273 ecd6f0ca62ea
child 30300 aa44d67eea16
equal deleted inserted replaced
30294:d6bffd97d8d5 30298:abefe1dfadbb
   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 * New predicate "strict_mono" classifies strict functions on partial orders.
       
   224 With strict functions on linear orders, reasoning about (in)equalities is
       
   225 facilitated by theorems "strict_mono_eq", "strict_mono_eq" and "strict_mono_eq".
   222 
   226 
   223 * Auxiliary class "itself" has disappeared -- classes without any parameter
   227 * Auxiliary class "itself" has disappeared -- classes without any parameter
   224 are treated as expected by the 'class' command.
   228 are treated as expected by the 'class' command.
   225 
   229 
   226 * Leibnitz's Series for Pi and the arcus tangens and logarithm series.
   230 * Leibnitz's Series for Pi and the arcus tangens and logarithm series.