equal
deleted
inserted
replaced
233 sizechange -> size_change |
233 sizechange -> size_change |
234 induct_scheme -> induction_schema |
234 induct_scheme -> induction_schema |
235 |
235 |
236 |
236 |
237 *** ML *** |
237 *** ML *** |
|
238 |
|
239 * Theory and context data is now introduced by the simplified and |
|
240 modernized functors Theory_Data, Proof_Data, Generic_Data. Data needs |
|
241 to be pure, but the old TheoryDataFun for mutable data (with explicit |
|
242 copy operation) is still available for some time. |
238 |
243 |
239 * Removed some old-style infix operations using polymorphic equality. |
244 * Removed some old-style infix operations using polymorphic equality. |
240 INCOMPATIBILITY. |
245 INCOMPATIBILITY. |
241 |
246 |
242 * Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML) |
247 * Structure Synchronized (cf. src/Pure/Concurrent/synchronized.ML) |