equal
deleted
inserted
replaced
158 contain multiple interpretations of local typedefs (with different |
158 contain multiple interpretations of local typedefs (with different |
159 non-emptiness proofs), even in a global theory context. |
159 non-emptiness proofs), even in a global theory context. |
160 |
160 |
161 * Theory Library/Coinductive_List has been removed -- superceded by |
161 * Theory Library/Coinductive_List has been removed -- superceded by |
162 AFP/thys/Coinductive. |
162 AFP/thys/Coinductive. |
|
163 |
|
164 * Theory PReal, including the type "preal" and related operations, has |
|
165 been removed. INCOMPATIBILITY. |
163 |
166 |
164 * Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin, |
167 * Split off theory Big_Operators containing setsum, setprod, Inf_fin, Sup_fin, |
165 Min, Max from theory Finite_Set. INCOMPATIBILITY. |
168 Min, Max from theory Finite_Set. INCOMPATIBILITY. |
166 |
169 |
167 * Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc. |
170 * Theory "Rational" renamed to "Rat", for consistency with "Nat", "Int" etc. |