equal
deleted
inserted
replaced
74 |
74 |
75 * HOL: Tactic emulation methods induct_tac and case_tac understand static |
75 * HOL: Tactic emulation methods induct_tac and case_tac understand static |
76 (Isar) contexts. |
76 (Isar) contexts. |
77 |
77 |
78 *** HOL *** |
78 *** HOL *** |
|
79 |
|
80 * Numerics: new theory Ring_and_Field contains over 250 basic numerical laws, |
|
81 all proved in axiomatic type classes for semirings, rings and fields. |
|
82 |
|
83 * Numerics: |
|
84 - Numeric types (nat, int, and in HOL-Complex rat, real, complex, etc.) are |
|
85 now formalized using the Ring_and_Field theory mentioned above. |
|
86 - INCOMPATIBILITY: simplification and arithmetic behaves somewhat differently |
|
87 than before, because now they are set up once in a generic manner. |
|
88 - INCOMPATIBILITY: many type-specific instances of laws proved in |
|
89 Ring_and_Field are no longer available. |
|
90 |
|
91 * Type "rat" of the rational numbers is now availabe in HOL-Complex. |
79 |
92 |
80 * Records: |
93 * Records: |
81 - Record types are now by default printed with their type abbreviation |
94 - Record types are now by default printed with their type abbreviation |
82 instead of the list of all field types. This can be configured via |
95 instead of the list of all field types. This can be configured via |
83 the reference "print_record_type_abbr". |
96 the reference "print_record_type_abbr". |