NEWS
changeset 10391 0025fd11882c
parent 10337 fca9cd9fd115
child 10401 58bb50f69497
equal deleted inserted replaced
10390:1d54567bed24 10391:0025fd11882c
     5 *** Overview of INCOMPATIBILITIES ***
     5 *** Overview of INCOMPATIBILITIES ***
     6 
     6 
     7 * HOL: induct renamed to lfp_induct;
     7 * HOL: induct renamed to lfp_induct;
     8 
     8 
     9 * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;
     9 * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;
       
    10 
       
    11 * Isar: 'obtain' no longer declares "that" fact as simp/intro;
    10 
    12 
    11 
    13 
    12 *** Document preparation ***
    14 *** Document preparation ***
    13 
    15 
    14 * improved isabelle style files; more abstract symbol implementation
    16 * improved isabelle style files; more abstract symbol implementation
    22 that presentation of goal states does not conform to actual
    24 that presentation of goal states does not conform to actual
    23 human-readable proof documents.  Please do not include goal states
    25 human-readable proof documents.  Please do not include goal states
    24 into document output unless you really know what you are doing!
    26 into document output unless you really know what you are doing!
    25 
    27 
    26 
    28 
    27 
       
    28 *** Isar ***
    29 *** Isar ***
    29 
    30 
    30 * HOL: default proof step now includes 'intro_classes';
    31 * Pure: assumption method (an implicit finishing) now handles actual
       
    32 rules as well;
       
    33 
       
    34 * Pure: improved 'obtain' --- moved to Pure, insert "that" into
       
    35 initial goal, declare "that" only as Pure intro (only for single
       
    36 steps); the "that" rule assumption may now be involved in implicit
       
    37 finishing, thus ".." becomes a feasible for trivial obtains;
       
    38 
       
    39 * Pure: default proof step now includes 'intro_classes'; thus trivial
       
    40 instance proofs may be performed by "..";
       
    41 
       
    42 * Pure: ?thesis / ?this / "..." now work for pure meta-level
       
    43 statements as well;
    31 
    44 
    32 
    45 
    33 *** HOL ***
    46 *** HOL ***
    34 
    47 
    35 * HOL/Library: a collection of generic theories to be used together
    48 * HOL/Library: a collection of generic theories to be used together
    36 with main HOL; the theory loader path already includes this directory
    49 with main HOL; the theory loader path already includes this directory
    37 by default; the following existing theories have been moved here:
    50 by default; the following existing theories have been moved here:
    38 HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
    51 HOL/Induct/Multiset, HOL/Induct/Acc (as Accessible_Part), HOL/While
    39 (as While_Combinator), HOL/Lex/Prefix (as List_Prefix);
    52 (as While_Combinator), HOL/Lex/Prefix (as List_Prefix);
       
    53 
       
    54 * HOL/typedef: simplified package, provide more useful rules (see also
       
    55 HOL/subset.thy);
       
    56 
       
    57 
       
    58 *** General ***
       
    59 
       
    60 * Provers: fast_tac (and friends) now handle actual object-logic rules
       
    61 as assumptions as well;
       
    62 
    40 
    63 
    41 
    64 
    42 New in Isabelle99-1 (October 2000)
    65 New in Isabelle99-1 (October 2000)
    43 ----------------------------------
    66 ----------------------------------
    44 
    67