* Pure/sign/theory: discontinued named name spaces;
authorwenzelm
Sat Jun 11 22:15:58 2005 +0200 (2005-06-11)
changeset 163739d020423093b
parent 16372 8618d334840b
child 16374 f4b7cf8975af
* Pure/sign/theory: discontinued named name spaces;
* Pure: Theory.axioms_of, PureThy.thms_of etc.;
NEWS
     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