author | wenzelm |

Sat Jun 11 22:15:58 2005 +0200 (2005-06-11) | |

changeset 16373 | 9d020423093b |

parent 16372 | 8618d334840b |

child 16374 | f4b7cf8975af |

* Pure/sign/theory: discontinued named name spaces;

* Pure: Theory.axioms_of, PureThy.thms_of etc.;

* Pure: Theory.axioms_of, PureThy.thms_of etc.;

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