equal
deleted
inserted
replaced
41 - The 'smt_oracle' option is now necessary when using the 'smt' method |
41 - The 'smt_oracle' option is now necessary when using the 'smt' method |
42 with a solver other than Z3. INCOMPATIBILITY. |
42 with a solver other than Z3. INCOMPATIBILITY. |
43 - The encoding to first-order logic is now more complete in the presence of |
43 - The encoding to first-order logic is now more complete in the presence of |
44 higher-order quantifiers. An 'smt_explicit_application' option has been |
44 higher-order quantifiers. An 'smt_explicit_application' option has been |
45 added to control this. INCOMPATIBILITY. |
45 added to control this. INCOMPATIBILITY. |
|
46 |
|
47 * Theory HOL-Computational_Algebra.Polynomial_Factorial does not |
|
48 provide instances of rat, real, complex as factorial rings etc. |
|
49 Import HOL-Computational_Algebra.Field_as_Ring explicitly in case of |
|
50 need. INCOMPATIBILITY. |
46 |
51 |
47 * Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid clash |
52 * Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid clash |
48 with fact mod_mult_self4 (on more generic semirings). INCOMPATIBILITY. |
53 with fact mod_mult_self4 (on more generic semirings). INCOMPATIBILITY. |
49 |
54 |
50 * Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to |
55 * Facts sum.commute(_restrict) and prod.commute(_restrict) renamed to |