NEWS
changeset 17016 73c74cb1d744
parent 16997 7dfc99f62dd9
child 17047 e2e2d75bb37b
equal deleted inserted replaced
17015:50e1d2be7e67 17016:73c74cb1d744
   259 Moreover, the mathematically important symbolic identifier \<epsilon>
   259 Moreover, the mathematically important symbolic identifier \<epsilon>
   260 becomes available as variable, constant etc.  INCOMPATIBILITY,
   260 becomes available as variable, constant etc.  INCOMPATIBILITY,
   261 
   261 
   262 * "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".
   262 * "x > y" abbreviates "y < x" and "x >= y" abbreviates "y <= x".
   263 Similarly for all quantifiers: "ALL x > y" etc.  The x-symbol for >=
   263 Similarly for all quantifiers: "ALL x > y" etc.  The x-symbol for >=
   264 is \<ge>.
   264 is \<ge>. New transitivity rules have been added to HOL/Orderings.thy to 
       
   265 support corresponding Isar calculations.
   265 
   266 
   266 * "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\<in>"
   267 * "{x:A. P}" abbreviates "{x. x:A & P}", and similarly for "\<in>"
   267 instead of ":".
   268 instead of ":".
   268 
   269 
   269 * theory SetInterval: changed the syntax for open intervals:
   270 * theory SetInterval: changed the syntax for open intervals:
   382 integers in the reals.
   383 integers in the reals.
   383 
   384 
   384 The following theorems have been eliminated or modified
   385 The following theorems have been eliminated or modified
   385 (INCOMPATIBILITY):
   386 (INCOMPATIBILITY):
   386 
   387 
   387   real_of_int_add    reversed direction of equality (use [symmetric])
   388   exp_ge_add_one_self  now requires no hypotheses
   388   real_of_int_minus  reversed direction of equality (use [symmetric])
   389   real_of_int_add      reversed direction of equality (use [symmetric])
   389   real_of_int_diff   reversed direction of equality (use [symmetric])
   390   real_of_int_minus    reversed direction of equality (use [symmetric])
   390   real_of_int_mult   reversed direction of equality (use [symmetric])
   391   real_of_int_diff     reversed direction of equality (use [symmetric])
       
   392   real_of_int_mult     reversed direction of equality (use [symmetric])
   391 
   393 
   392 * Theory RComplete: expanded support for floor and ceiling functions.
   394 * Theory RComplete: expanded support for floor and ceiling functions.
   393 
   395 
   394 * Theory Ln is new, with properties of the natural logarithm
   396 * Theory Ln is new, with properties of the natural logarithm
   395 
   397