equal
deleted
inserted
replaced
320 * Pure/General: rat.ML implements rational numbers. |
320 * Pure/General: rat.ML implements rational numbers. |
321 |
321 |
322 * Pure: datatype Context.generic joins theory/Proof.context and |
322 * Pure: datatype Context.generic joins theory/Proof.context and |
323 provides some facilities for code that works in either kind of |
323 provides some facilities for code that works in either kind of |
324 context, notably GenericDataFun for uniform theory and proof data. |
324 context, notably GenericDataFun for uniform theory and proof data. |
|
325 |
|
326 * Pure: 'advanced' translation functions (parse_translation etc.) now |
|
327 use Context.generic instead of just theory. |
325 |
328 |
326 * Pure: simplified internal attribute type, which is now always |
329 * Pure: simplified internal attribute type, which is now always |
327 Context.generic * thm -> Context.generic * thm. Global (theory) |
330 Context.generic * thm -> Context.generic * thm. Global (theory) |
328 vs. local (Proof.context) attributes have been discontinued, while |
331 vs. local (Proof.context) attributes have been discontinued, while |
329 minimizing code duplication. Thm.rule_attribute and |
332 minimizing code duplication. Thm.rule_attribute and |