equal
deleted
inserted
replaced
96 Isabelle/Scala, with simplified arguments and explicit errors from the |
96 Isabelle/Scala, with simplified arguments and explicit errors from the |
97 latex and bibtex process. Minor INCOMPATIBILITY. |
97 latex and bibtex process. Minor INCOMPATIBILITY. |
98 |
98 |
99 |
99 |
100 *** HOL *** |
100 *** HOL *** |
|
101 |
|
102 * A new command parametric_constant for proving parametricity of |
|
103 non-recursive definitions. For constants that are not fully parametric the |
|
104 command will infer conditions on relations (e.g., bi_unique, bi_total, or |
|
105 type class conditions such as "respects 0") sufficient for parametricity. |
|
106 See ~~/src/HOL/ex/Conditional_Parametricity_Examples for some examples. |
101 |
107 |
102 * SMT module: |
108 * SMT module: |
103 - The 'smt_oracle' option is now necessary when using the 'smt' method |
109 - The 'smt_oracle' option is now necessary when using the 'smt' method |
104 with a solver other than Z3. INCOMPATIBILITY. |
110 with a solver other than Z3. INCOMPATIBILITY. |
105 - The encoding to first-order logic is now more complete in the |
111 - The encoding to first-order logic is now more complete in the |