equal
deleted
inserted
replaced
136 |
136 |
137 * Local_Theory.reset is no longer available in user space. Regular |
137 * Local_Theory.reset is no longer available in user space. Regular |
138 definitional packages should use balanced blocks of |
138 definitional packages should use balanced blocks of |
139 Local_Theory.open_target versus Local_Theory.close_target instead, |
139 Local_Theory.open_target versus Local_Theory.close_target instead, |
140 or the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY. |
140 or the Local_Theory.subtarget(_result) combinator. Rare INCOMPATIBILITY. |
|
141 |
|
142 * Slightly more conventional naming schema in structure Inductive. |
|
143 Minor INCOMPATIBILITY. |
141 |
144 |
142 * Original PolyML.pointerEq is retained as a convenience for tools that |
145 * Original PolyML.pointerEq is retained as a convenience for tools that |
143 don't use Isabelle/ML (where this is called "pointer_eq"). |
146 don't use Isabelle/ML (where this is called "pointer_eq"). |
144 |
147 |
145 * ML evaluation (notably via commands 'ML' and 'ML_file') is subject to |
148 * ML evaluation (notably via commands 'ML' and 'ML_file') is subject to |