* Pure: get_thm interface expects datatype thmref;
authorwenzelm
Mon Jun 20 22:14:21 2005 +0200 (2005-06-20)
changeset 16506b2687ce38433
parent 16505 c4b2e3cd84ab
child 16507 ee552def8721
* Pure: get_thm interface expects datatype thmref;
* More efficient treatment of intermediate theory checkpoints;
NEWS
     1.1 --- a/NEWS	Mon Jun 20 22:14:20 2005 +0200
     1.2 +++ b/NEWS	Mon Jun 20 22:14:21 2005 +0200
     1.3 @@ -161,6 +161,9 @@
     1.4  * New syntax 'name(i-j, i-, i, ...)' for referring to specific
     1.5  selections of theorems in named facts via index ranges.
     1.6  
     1.7 +* More efficient treatment of intermediate checkpoints in interactive
     1.8 +theory development.
     1.9 +
    1.10  
    1.11  *** Locales ***
    1.12    
    1.13 @@ -459,6 +462,10 @@
    1.14  Theory.hide_classes_i/types_i/consts_i, while the non '_i' versions
    1.15  internalize their arguments!  INCOMPATIBILITY.
    1.16  
    1.17 +* Pure: get_thm interface (of PureThy and ProofContext) expects
    1.18 +datatype thmref (with constructors Name and NameSelection) instead of
    1.19 +plain string -- INCOMPATIBILITY;
    1.20 +
    1.21  * Pure: cases produced by proof methods specify options, where NONE
    1.22  means to remove case bindings -- INCOMPATIBILITY in
    1.23  (RAW_)METHOD_CASES.