equal
deleted
inserted
replaced
151 INCOMPATIBILITY: Rewrite propositions with "S O R" --> "R O S". Proofs |
151 INCOMPATIBILITY: Rewrite propositions with "S O R" --> "R O S". Proofs |
152 may occationally break, since the O_assoc rule was not rewritten like |
152 may occationally break, since the O_assoc rule was not rewritten like |
153 this. Fix using O_assoc[symmetric]. The same applies to the curried |
153 this. Fix using O_assoc[symmetric]. The same applies to the curried |
154 version "R OO S". |
154 version "R OO S". |
155 |
155 |
156 * Function "Inv" is renamed to "inv_onto" and function "inv" is now an |
156 * Function "Inv" is renamed to "inv_into" and function "inv" is now an |
157 abbreviation for "inv_onto UNIV". Lemmas are renamed accordingly. |
157 abbreviation for "inv_into UNIV". Lemmas are renamed accordingly. |
158 INCOMPATIBILITY. |
158 INCOMPATIBILITY. |
159 |
159 |
160 * ML antiquotation @{code_datatype} inserts definition of a datatype |
160 * ML antiquotation @{code_datatype} inserts definition of a datatype |
161 generated by the code generator; see Predicate.thy for an example. |
161 generated by the code generator; see Predicate.thy for an example. |
162 |
162 |