equal
deleted
inserted
replaced
96 * Numerics: |
96 * Numerics: |
97 - Numeric types (nat, int, and in HOL-Complex rat, real, complex, etc.) are |
97 - Numeric types (nat, int, and in HOL-Complex rat, real, complex, etc.) are |
98 now formalized using the Ring_and_Field theory mentioned above. |
98 now formalized using the Ring_and_Field theory mentioned above. |
99 - INCOMPATIBILITY: simplification and arithmetic behaves somewhat differently |
99 - INCOMPATIBILITY: simplification and arithmetic behaves somewhat differently |
100 than before, because now they are set up once in a generic manner. |
100 than before, because now they are set up once in a generic manner. |
101 - INCOMPATIBILITY: many type-specific instances of laws proved in |
101 - INCOMPATIBILITY: many type-specific arithmetic laws have gone. |
102 Ring_and_Field are no longer available. |
102 Look for the general versions in Ring_and_Field (and Power if they concern |
|
103 exponentiation). |
103 |
104 |
104 * Type "rat" of the rational numbers is now available in HOL-Complex. |
105 * Type "rat" of the rational numbers is now available in HOL-Complex. |
105 |
106 |
106 * Records: |
107 * Records: |
107 - Record types are now by default printed with their type abbreviation |
108 - Record types are now by default printed with their type abbreviation |