summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

Sat, 08 Jul 2006 12:54:26 +0200 | |

changeset 20040 | 02c59ec2f2e1 |

parent 20039 | 4293f932fe83 |

child 20041 | ae7aba935986 |

* Pure: structure Variable provides operations for proper treatment of fixed/schematic variables;
* Pure: Goal.prove, Goal.prove_global;
tuned;

--- a/NEWS Fri Jul 07 18:13:58 2006 +0200 +++ b/NEWS Sat Jul 08 12:54:26 2006 +0200 @@ -563,10 +563,6 @@ signature declarations. (This information is not relevant to the logic, but only for type inference.) IMPORTANT INTERNAL CHANGE. -* Pure: Logic.(un)varify only works in a global context, which is now -enforced instead of silently assumed. INCOMPATIBILITY, may use -Logic.legacy_(un)varify as temporary workaround. - * Pure: axiomatic type classes are now purely definitional, with explicit proofs of class axioms and super class relations performed internally. See Pure/axclass.ML for the main internal interfaces -- @@ -593,11 +589,24 @@ slightly more general idea of ``protecting'' meta-level rule statements. +* Pure: Logic.(un)varify only works in a global context, which is now +enforced instead of silently assumed. INCOMPATIBILITY, may use +Logic.legacy_(un)varify as temporary workaround. + +* Pure: structure Variable provides fundamental operations for proper +treatment of fixed/schematic variables in a context. For example, +Variable.import introduces fixes for schematics of given facts and +Variable.export reverses the effect (up to renaming) -- this replaces +various freeze_thaw operations. + * Pure: structure Goal provides simple interfaces for init/conclude/finish and tactical prove operations (replacing former -Tactic.prove). Note that OldGoals.prove_goalw_cterm has long been -obsolete, it is ill-behaved in a local proof context (e.g. with local -fixes/assumes or in a locale context). +Tactic.prove). Goal.prove is the canonical way to prove results +within a given context; Goal.prove_global is a degraded version for +theory level goals, including a global Drule.standard. Note that +OldGoals.prove_goalw_cterm has long been obsolete, since it is +ill-behaved in a local proof context (e.g. with local fixes/assumes or +in a locale context). * Isar: simplified treatment of user-level errors, using exception ERROR of string uniformly. Function error now merely raises ERROR,