equal
deleted
inserted
replaced
48 large (cf. Poly/ML option -H). (Requires Poly/ML 5.2.1 or later.) |
48 large (cf. Poly/ML option -H). (Requires Poly/ML 5.2.1 or later.) |
49 |
49 |
50 * The main reference manuals ("isar-ref", "implementation", and |
50 * The main reference manuals ("isar-ref", "implementation", and |
51 "system") have been updated and extended. Formally checked references |
51 "system") have been updated and extended. Formally checked references |
52 as hyperlinks are now available uniformly. |
52 as hyperlinks are now available uniformly. |
53 |
|
54 |
53 |
55 |
54 |
56 *** Pure *** |
55 *** Pure *** |
57 |
56 |
58 * Complete re-implementation of locales. INCOMPATIBILITY in several |
57 * Complete re-implementation of locales. INCOMPATIBILITY in several |
608 least_carrier ~> least_closed |
607 least_carrier ~> least_closed |
609 greatest_carrier ~> greatest_closed |
608 greatest_carrier ~> greatest_closed |
610 greatest_Lower_above ~> greatest_Lower_below |
609 greatest_Lower_above ~> greatest_Lower_below |
611 one_zero ~> carrier_one_zero |
610 one_zero ~> carrier_one_zero |
612 one_not_zero ~> carrier_one_not_zero (collision with assumption) |
611 one_not_zero ~> carrier_one_not_zero (collision with assumption) |
|
612 |
|
613 |
|
614 *** HOL-Nominal *** |
|
615 |
|
616 * Modernized versions of commands 'nominal_inductive', |
|
617 'nominal_primrec', and 'equivariance' work with local theory targets. |
613 |
618 |
614 |
619 |
615 *** HOLCF *** |
620 *** HOLCF *** |
616 |
621 |
617 * Reimplemented the simplification procedure for proving continuity |
622 * Reimplemented the simplification procedure for proving continuity |