equal
deleted
inserted
replaced
166 Isabelle/Scala, with simplified arguments and explicit errors from the |
166 Isabelle/Scala, with simplified arguments and explicit errors from the |
167 latex and bibtex process. Minor INCOMPATIBILITY. |
167 latex and bibtex process. Minor INCOMPATIBILITY. |
168 |
168 |
169 |
169 |
170 *** HOL *** |
170 *** HOL *** |
|
171 |
|
172 * Clarifed theorem names: |
|
173 |
|
174 Min.antimono ~> Min.subset_imp |
|
175 Max.antimono ~> Max.subset_imp |
|
176 |
|
177 Minor INCOMPATIBILITY. |
171 |
178 |
172 * A new command parametric_constant for proving parametricity of |
179 * A new command parametric_constant for proving parametricity of |
173 non-recursive definitions. For constants that are not fully parametric |
180 non-recursive definitions. For constants that are not fully parametric |
174 the command will infer conditions on relations (e.g., bi_unique, |
181 the command will infer conditions on relations (e.g., bi_unique, |
175 bi_total, or type class conditions such as "respects 0") sufficient for |
182 bi_total, or type class conditions such as "respects 0") sufficient for |