equal
deleted
inserted
replaced
416 to "split_conv" (old name still available for compatibility); |
416 to "split_conv" (old name still available for compatibility); |
417 |
417 |
418 * HOL: improved concrete syntax for strings (e.g. allows translation |
418 * HOL: improved concrete syntax for strings (e.g. allows translation |
419 rules with string literals); |
419 rules with string literals); |
420 |
420 |
421 * HOL-Hyperreal: a new target, extending HOL-Real with the hyperreals |
421 * HOL-Real-Hyperreal: this extends HOL-Real with the hyperreals |
422 and Fleuriot's mechanization of analysis; |
422 and Fleuriot's mechanization of analysis, including the transcendental |
|
423 functions for the reals; |
423 |
424 |
424 * HOL/Real, HOL/Hyperreal: improved arithmetic simplification; |
425 * HOL/Real, HOL/Hyperreal: improved arithmetic simplification; |
425 |
426 |
426 |
427 |
427 *** CTT *** |
428 *** CTT *** |