equal
deleted
inserted
replaced
179 |
179 |
180 |
180 |
181 *** ML *** |
181 *** ML *** |
182 |
182 |
183 * Generic Toplevel.add_hook interface allows to analyze the result of |
183 * Generic Toplevel.add_hook interface allows to analyze the result of |
184 transactions (including failed ones). For example, see |
184 transactions. E.g. see src/Pure/ProofGeneral/proof_general_pgip.ML |
185 src/Pure/ProofGeneral/proof_general_pgip.ML for theorem dependency |
185 for theorem dependency output of transactions resulting in a new |
186 output of transactions resulting in a new theory state. |
186 theory state. |
187 |
187 |
188 * Name bindings in higher specification mechanisms (notably |
188 * Name bindings in higher specification mechanisms (notably |
189 LocalTheory.define, LocalTheory.note, and derived packages) are now |
189 LocalTheory.define, LocalTheory.note, and derived packages) are now |
190 formalized as type Name.binding, replacing old bstring. |
190 formalized as type Name.binding, replacing old bstring. |
191 INCOMPATIBILITY, need to wrap strings via Name.binding function, see |
191 INCOMPATIBILITY, need to wrap strings via Name.binding function, see |