misc stuff;
authorwenzelm
Sat Nov 04 18:39:44 2000 +0100 (2000-11-04)
changeset 103910025fd11882c
parent 10390 1d54567bed24
child 10392 f27afee8475d
misc stuff;
NEWS
     1.1 --- a/NEWS	Fri Nov 03 21:35:59 2000 +0100
     1.2 +++ b/NEWS	Sat Nov 04 18:39:44 2000 +0100
     1.3 @@ -8,6 +8,8 @@
     1.4  
     1.5  * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;
     1.6  
     1.7 +* Isar: 'obtain' no longer declares "that" fact as simp/intro;
     1.8 +
     1.9  
    1.10  *** Document preparation ***
    1.11  
    1.12 @@ -24,10 +26,21 @@
    1.13  into document output unless you really know what you are doing!
    1.14  
    1.15  
    1.16 -
    1.17  *** Isar ***
    1.18  
    1.19 -* HOL: default proof step now includes 'intro_classes';
    1.20 +* Pure: assumption method (an implicit finishing) now handles actual
    1.21 +rules as well;
    1.22 +
    1.23 +* Pure: improved 'obtain' --- moved to Pure, insert "that" into
    1.24 +initial goal, declare "that" only as Pure intro (only for single
    1.25 +steps); the "that" rule assumption may now be involved in implicit
    1.26 +finishing, thus ".." becomes a feasible for trivial obtains;
    1.27 +
    1.28 +* Pure: default proof step now includes 'intro_classes'; thus trivial
    1.29 +instance proofs may be performed by "..";
    1.30 +
    1.31 +* Pure: ?thesis / ?this / "..." now work for pure meta-level
    1.32 +statements as well;
    1.33  
    1.34  
    1.35  *** HOL ***
    1.36 @@ -38,6 +51,16 @@
    1.37  HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
    1.38  (as While_Combinator), HOL/Lex/Prefix (as List_Prefix);
    1.39  
    1.40 +* HOL/typedef: simplified package, provide more useful rules (see also
    1.41 +HOL/subset.thy);
    1.42 +
    1.43 +
    1.44 +*** General ***
    1.45 +
    1.46 +* Provers: fast_tac (and friends) now handle actual object-logic rules
    1.47 +as assumptions as well;
    1.48 +
    1.49 +
    1.50  
    1.51  New in Isabelle99-1 (October 2000)
    1.52  ----------------------------------