equal
deleted
inserted
replaced
118 |
118 |
119 |
119 |
120 *** HOL *** |
120 *** HOL *** |
121 |
121 |
122 * A new command parametric_constant for proving parametricity of |
122 * A new command parametric_constant for proving parametricity of |
123 non-recursive definitions. For constants that are not fully parametric the |
123 non-recursive definitions. For constants that are not fully parametric |
124 command will infer conditions on relations (e.g., bi_unique, bi_total, or |
124 the command will infer conditions on relations (e.g., bi_unique, |
125 type class conditions such as "respects 0") sufficient for parametricity. |
125 bi_total, or type class conditions such as "respects 0") sufficient for |
126 See ~~/src/HOL/ex/Conditional_Parametricity_Examples for some examples. |
126 parametricity. See ~~/src/HOL/ex/Conditional_Parametricity_Examples for |
|
127 some examples. |
127 |
128 |
128 * SMT module: |
129 * SMT module: |
129 - The 'smt_oracle' option is now necessary when using the 'smt' method |
130 - The 'smt_oracle' option is now necessary when using the 'smt' method |
130 with a solver other than Z3. INCOMPATIBILITY. |
131 with a solver other than Z3. INCOMPATIBILITY. |
131 - The encoding to first-order logic is now more complete in the |
132 - The encoding to first-order logic is now more complete in the |