equal
deleted
inserted
replaced
143 - The 'smt_oracle' option is now necessary when using the 'smt' method |
143 - The 'smt_oracle' option is now necessary when using the 'smt' method |
144 with a solver other than Z3. INCOMPATIBILITY. |
144 with a solver other than Z3. INCOMPATIBILITY. |
145 - The encoding to first-order logic is now more complete in the |
145 - The encoding to first-order logic is now more complete in the |
146 presence of higher-order quantifiers. An 'smt_explicit_application' |
146 presence of higher-order quantifiers. An 'smt_explicit_application' |
147 option has been added to control this. INCOMPATIBILITY. |
147 option has been added to control this. INCOMPATIBILITY. |
|
148 |
|
149 * Datatypes: |
|
150 - The legacy command 'old_datatype', provided by |
|
151 '~~/src/HOL/Library/Old_Datatype.thy', has been removed. INCOMPATIBILITY. |
148 |
152 |
149 * Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide |
153 * Theory HOL-Computational_Algebra.Polynomial_Factorial does not provide |
150 instances of rat, real, complex as factorial rings etc. Import |
154 instances of rat, real, complex as factorial rings etc. Import |
151 HOL-Computational_Algebra.Field_as_Ring explicitly in case of need. |
155 HOL-Computational_Algebra.Field_as_Ring explicitly in case of need. |
152 INCOMPATIBILITY. |
156 INCOMPATIBILITY. |