equal
deleted
inserted
replaced
385 real_of_int_minus reversed direction of equality (use [symmetric]) |
385 real_of_int_minus reversed direction of equality (use [symmetric]) |
386 real_of_int_diff reversed direction of equality (use [symmetric]) |
386 real_of_int_diff reversed direction of equality (use [symmetric]) |
387 real_of_int_mult reversed direction of equality (use [symmetric]) |
387 real_of_int_mult reversed direction of equality (use [symmetric]) |
388 |
388 |
389 * Theory RComplete: expanded support for floor and ceiling functions. |
389 * Theory RComplete: expanded support for floor and ceiling functions. |
|
390 |
|
391 |
|
392 *** HOL-Library *** |
|
393 |
|
394 * Theories SetsAndFunctions and BigO support asymptotic "big O" calculations. |
|
395 See the notes in BigO.thy. |
390 |
396 |
391 |
397 |
392 *** HOLCF *** |
398 *** HOLCF *** |
393 |
399 |
394 * HOLCF: discontinued special version of 'constdefs' (which used to |
400 * HOLCF: discontinued special version of 'constdefs' (which used to |