372 * Pure: simplified internal attribute type, which is now always |
372 * Pure: simplified internal attribute type, which is now always |
373 Context.generic * thm -> Context.generic * thm. Global (theory) |
373 Context.generic * thm -> Context.generic * thm. Global (theory) |
374 vs. local (Proof.context) attributes have been discontinued, while |
374 vs. local (Proof.context) attributes have been discontinued, while |
375 minimizing code duplication. Thm.rule_attribute and |
375 minimizing code duplication. Thm.rule_attribute and |
376 Thm.declaration_attribute build canonical attributes; see also |
376 Thm.declaration_attribute build canonical attributes; see also |
377 structure Context for further operations on Context.generic. |
377 structure Context for further operations on Context.generic, notably |
378 |
378 GenericDataFun. INCOMPATIBILITY, need to adapt attribute type |
379 INCOMPATIBILITY, need to adapt attribute type declarations and |
379 declarations and definitions. |
380 definitions. Hint: make proper use of GenericDataFun and generic |
380 |
381 Args/Attrib syntax instead of working around legacy code. |
381 * Pure/Isar: Args/Attrib parsers operate on Context.generic -- |
|
382 global/local versions on theory vs. Proof.context have been |
|
383 discontinued; Attrib.syntax and Method.syntax have been adapted |
|
384 accordingly. INCOMPATIBILITY, need to adapt parser expressions for |
|
385 attributes, methods, etc. |
382 |
386 |
383 * Pure: several functions of signature "... -> theory -> theory * ..." |
387 * Pure: several functions of signature "... -> theory -> theory * ..." |
384 have been reoriented to "... -> theory -> ... * theory" in order to |
388 have been reoriented to "... -> theory -> ... * theory" in order to |
385 allow natural usage in combination with the ||>, ||>>, |-> and |
389 allow natural usage in combination with the ||>, ||>>, |-> and |
386 fold_map combinators. |
390 fold_map combinators. |