NEWS
changeset 10858 479dad7b3b41
parent 10856 e8a5340418b6
child 10862 857688d775b0
     1.1 --- a/NEWS	Wed Jan 10 17:21:31 2001 +0100
     1.2 +++ b/NEWS	Wed Jan 10 20:18:55 2001 +0100
     1.3 @@ -1,22 +1,21 @@
     1.4 +
     1.5  Isabelle NEWS -- history user-relevant changes
     1.6  ==============================================
     1.7  
     1.8  *** Overview of INCOMPATIBILITIES ***
     1.9  
    1.10  * HOL/Real: "rinv" and "hrinv" replaced by overloaded "inverse"
    1.11 -function;
    1.12 +operation;
    1.13  
    1.14  * HOL: induct renamed to lfp_induct;
    1.15  
    1.16  * HOL: contrapos, contrapos2 renamed to contrapos_nn, contrapos_pp;
    1.17  
    1.18 -* HOL: infix "dvd" now has priority 50 rather than 70
    1.19 -  (because it is a relation)
    1.20 -  infix ^^ has been renamed ``
    1.21 -  infix `` has been renamed `
    1.22 -  "univalent" has been renamed "single_valued"
    1.23 +* HOL: infix "dvd" now has priority 50 rather than 70 (because it is a
    1.24 +relation); infix "^^" has been renamed "``"; infix "``" has been
    1.25 +renamed "`"; "univalent" has been renamed "single_valued";
    1.26  
    1.27 -* HOLCF: infix ` has been renamed $
    1.28 +* HOLCF: infix "`" has been renamed "$";
    1.29  
    1.30  * Isar: 'obtain' no longer declares "that" fact as simp/intro;
    1.31  
    1.32 @@ -31,9 +30,18 @@
    1.33  (should now use \isamath{...} and \isatext{...} in custom symbol
    1.34  definitions);
    1.35  
    1.36 +* \isabellestyle{NAME} selects version of Isabelle output (currently
    1.37 +available: are "it" for near math-mode best-style output, "sl" for
    1.38 +slanted text style, and "tt" for plain type-writer; if no
    1.39 +\isabellestyle command is given, output is according to slanted
    1.40 +type-writer);
    1.41 +
    1.42  * support sub/super scripts (for single symbols only), input syntax is
    1.43  like this: "A\<^sup>*" or "A\<^sup>\<star>";
    1.44  
    1.45 +* some more standard symbols; see Appendix A of the system manual for
    1.46 +the complete list;
    1.47 +
    1.48  * antiquotation @{goals} and @{subgoals} for output of *dynamic* goals
    1.49  state; Note that presentation of goal states does not conform to
    1.50  actual human-readable proof documents.  Please do not include goal
    1.51 @@ -62,6 +70,12 @@
    1.52  * Pure: ?thesis / ?this / "..." now work for pure meta-level
    1.53  statements as well;
    1.54  
    1.55 +* Pure: the builtin notion of 'finished' goal now includes the ==-refl
    1.56 +rule (as well as the assumption rule);
    1.57 +
    1.58 +* Pure: 'thm_deps' command visualizes dependencies of theorems and
    1.59 +lemmas, using the graph browser tool;
    1.60 +
    1.61  * HOL: improved method 'induct' --- now handles non-atomic goals
    1.62  (potential INCOMPATIBILITY); tuned error handling;
    1.63  
    1.64 @@ -69,6 +83,10 @@
    1.65  number of facts to be consumed (0 for "type" and 1 for "set" rules);
    1.66  any remaining facts are inserted into the goal verbatim;
    1.67  
    1.68 +* HOL: local contexts (aka cases) may now contain term bindings as
    1.69 +well; the 'cases' and 'induct' methods new provide a ?case binding for
    1.70 +the result to be shown in each case;
    1.71 +
    1.72  * HOL: added 'recdef_tc' command;
    1.73  
    1.74  
    1.75 @@ -92,6 +110,7 @@
    1.76  
    1.77  * HOL-Real, HOL-Hyperreals: improved arithmetic simplification;
    1.78  
    1.79 +
    1.80  *** CTT ***
    1.81  
    1.82  * CTT: x-symbol support for Pi, Sigma, -->, : (membership); note that