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

author | wenzelm |

Sat, 11 Jun 2005 22:15:58 +0200 | |

changeset 16373 | 9d020423093b |

parent 16372 | 8618d334840b |

child 16374 | f4b7cf8975af |

* Pure/sign/theory: discontinued named name spaces;
* Pure: Theory.axioms_of, PureThy.thms_of etc.;

--- a/NEWS Sat Jun 11 22:15:57 2005 +0200 +++ b/NEWS Sat Jun 11 22:15:58 2005 +0200 @@ -424,10 +424,27 @@ the original result when interning again, even if there is an overlap with earlier declarations. +* Pure/sign/theory: discontinued named name spaces (i.e. classK, +typeK, constK, axiomK, oracleK), but provide explicit operations for +any of these kinds. For example, Sign.intern typeK is now +Sign.intern_type, Theory.hide_space Sign.typeK is now +Theory.hide_types. Also note that former +Theory.hide_classes/types/consts are now +Theory.hide_classes_i/types_i/consts_i, while the non '_i' versions +internalize their arguments! INCOMPATIBILITY. + * Pure: cases produced by proof methods specify options, where NONE means to remove case bindings -- INCOMPATIBILITY in (RAW_)METHOD_CASES. +* Pure: the following operations retrieve axioms or theorems from a +theory node or theory hierarchy, respectively: + + Theory.axioms_of: theory -> (string * term) list + Theory.all_axioms_of: theory -> (string * term) list + PureThy.thms_of: theory -> (string * thm) list + PureThy.all_thms_of: theory -> (string * thm) list + * Provers: Simplifier and Classical Reasoner now support proof context dependent plug-ins (simprocs, solvers, wrappers etc.). These extra components are stored in the theory and patched into the