NEWS
changeset 16962 f99dd1274c5f
parent 16929 b23c54fd31f7
child 16997 7dfc99f62dd9
equal deleted inserted replaced
16961:9c5871b16553 16962:f99dd1274c5f
   388   real_of_int_minus  reversed direction of equality (use [symmetric])
   388   real_of_int_minus  reversed direction of equality (use [symmetric])
   389   real_of_int_diff   reversed direction of equality (use [symmetric])
   389   real_of_int_diff   reversed direction of equality (use [symmetric])
   390   real_of_int_mult   reversed direction of equality (use [symmetric])
   390   real_of_int_mult   reversed direction of equality (use [symmetric])
   391 
   391 
   392 * Theory RComplete: expanded support for floor and ceiling functions.
   392 * Theory RComplete: expanded support for floor and ceiling functions.
       
   393 
       
   394 * Theory Ln is new, with properties of the natural logarithm
   393 
   395 
   394 
   396 
   395 *** HOLCF ***
   397 *** HOLCF ***
   396 
   398 
   397 * HOLCF: discontinued special version of 'constdefs' (which used to
   399 * HOLCF: discontinued special version of 'constdefs' (which used to