equal
deleted
inserted
replaced
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 xsymbol for >= 
263 Similarly for all quantifiers: "ALL x > y" etc. The xsymbol 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 