1.1 --- a/NEWS	Wed Aug 16 18:10:15 2000 +0200
     1.2 +++ b/NEWS	Thu Aug 17 10:29:23 2000 +0200
     1.3 @@ -54,6 +54,10 @@
     1.4  
     1.5  * Isar: changed syntax of local blocks from {{ }} to { };
     1.6  
     1.7 +* Isar: renamed 'RS' attribute to 'THEN';
     1.8 +
     1.9 +* Isar/HOL: renamed "intrs" to "intros" in inductive definitions;
    1.10 +
    1.11  * Provers: strengthened force_tac by using new first_best_tac;
    1.12  
    1.13  * Provers: Blast_tac now warns of and ignores "weak elimination rules" e.g.
    1.14 @@ -130,12 +134,14 @@
    1.15  
    1.16  * Pure: changed syntax of local blocks from {{ }} to { };
    1.17  
    1.18 +* Pure: renamed 'RS' attribute to 'THEN';
    1.19 +
    1.20  * Pure: syntax of sorts made 'inner', i.e. have to write "{a, b, c}"
    1.21  instead of {a, b, c};
    1.22  
    1.23  * Pure now provides its own version of intro/elim/dest attributes;
    1.24  useful for building new logics, but beware of confusion with the
    1.25 -Provers/classical ones;
    1.26 +version in Provers/classical;
    1.27  
    1.28  * Pure: the local context of (non-atomic) goals is provided via case
    1.29  name 'antecedent';
    1.30 @@ -146,10 +152,18 @@
    1.31  * Pure: theory command 'method_setup' provides a simple interface for
    1.32  definining proof methods in ML;
    1.33  
    1.34 +* Provers: hypsubst support; also plain subst and symmetric attribute
    1.35 +(the latter supercedes [RS sym]);
    1.36 +
    1.37  * Provers: splitter support (via 'split' attribute and 'simp' method
    1.38  modifier); 'simp' method: 'only:' modifier removes loopers as well
    1.39  (including splits);
    1.40  
    1.41 +* Provers: added 'fastsimp' and 'clarsimp' methods (combination of
    1.42 +Simplifier and Classical reasoner);
    1.43 +
    1.44 +* Provers: added 'arith_split' attribute;
    1.45 +
    1.46  * HOL: new proof method 'cases' and improved version of 'induct' now
    1.47  support named cases; major packages (inductive, datatype, primrec,
    1.48  recdef) support case names and properly name parameters;
    1.49 @@ -157,19 +171,24 @@
    1.50  * HOL: removed 'case_split' thm binding, should use 'cases' proof
    1.51  method anyway;
    1.52  
    1.53 -* HOL/Calculation: new rules for substitution in inequalities
    1.54 -(monotonicity conditions are extracted to be proven at end);
    1.55 -
    1.56  * HOL: removed obsolete expand_if = split_if; theorems if_splits =
    1.57  split_if split_if_asm; datatype package provides theorems foo.splits =
    1.58  foo.split foo.split_asm for each datatype;
    1.59  
    1.60 -* names of theorems etc. may be natural numbers as well;
    1.61 +* HOL/Calculation: new rules for substitution in inequalities
    1.62 +(monotonicity conditions are extracted to be proven at end);
    1.63 +
    1.64 +* HOL/inductive: rename "intrs" to "intros" (potential
    1.65 +INCOMPATIBILITY); emulation of mk_cases feature for proof scripts:
    1.66 +'inductive_cases' command and 'ind_cases' method; NOTE: use (cases
    1.67 +(simplified)) method in proper proofs;
    1.68  
    1.69  * Provers: intro/elim/dest attributes: changed intro/intro!/intro!!
    1.70  flags to intro!/intro/intro? (in most cases, one should have to change
    1.71  intro!! to intro? only);
    1.72  
    1.73 +* names of theorems etc. may be natural numbers as well;
    1.74 +
    1.75  * 'pr' command: optional goals_limit argument; no longer prints theory
    1.76  contexts, but only proof states;
    1.77  
    1.78 @@ -178,8 +197,9 @@
    1.79  proof state according to the Isabelle LaTeX style;
    1.80  
    1.81  * improved support for emulating tactic scripts, including proof
    1.82 -methods 'tactic', 'res_inst_tac' etc., 'subgoal_tac', and 'case_tac' /
    1.83 -'induct_tac' (for HOL datatypes);
    1.84 +methods 'rule_tac' etc., 'cut_tac', 'thin_tac', 'subgoal_tac',
    1.85 +'rename_tac', 'rotate_tac', 'tactic', and 'case_tac' / 'induct_tac'
    1.86 +(for HOL datatypes);
    1.87  
    1.88  * simplified (more robust) goal selection of proof methods: 1st goal,
    1.89  all goals, or explicit goal specifier (tactic emulation); thus 'proof
    1.90 @@ -213,8 +233,9 @@
    1.91  
    1.92  * HOL/Real: "rabs" replaced by overloaded "abs" function;
    1.93  
    1.94 -* HOL/record: fixed select-update simplification procedure to handle
    1.95 -extended records as well; admit "r" as field name;
    1.96 +* HOL/record: added general record equality rule to simpset; fixed
    1.97 +select-update simplification procedure to handle extended records as
    1.98 +well; admit "r" as field name;
    1.99  
   1.100  * HOL: 0 is now overloaded over the new sort "zero", allowing its use with
   1.101  other numeric types and also as the identity of groups, rings, etc.;
   1.102 @@ -379,11 +400,11 @@
   1.103  reasoning); for further information see isatool doc isar-ref,
   1.104  src/HOL/Isar_examples and http://isabelle.in.tum.de/Isar/
   1.105  
   1.106 -* improved presentation of theories: better HTML markup (including
   1.107 -colors), graph views in several sizes; isatool usedir now provides a
   1.108 -proper interface for user theories (via -P option); actual document
   1.109 -preparation based on (PDF)LaTeX is available as well (for new-style
   1.110 -theories only); see isatool doc system for more information;
   1.111 +* improved and simplified presentation of theories: better HTML markup
   1.112 +(including colors), graph views in several sizes; isatool usedir now
   1.113 +provides a proper interface for user theories (via -P option); actual
   1.114 +document preparation based on (PDF)LaTeX is available as well (for
   1.115 +new-style theories only); see isatool doc system for more information;
   1.116  
   1.117  * native support for Proof General, both for classic Isabelle and
   1.118  Isabelle/Isar;