Isar: splitter support; improved diagnostics;
authorwenzelm
Thu Mar 16 00:31:58 2000 +0100 (2000-03-16)
changeset 84875f3b0e02ec15
parent 8486 85f504900ed5
child 8488 58e37d59c146
Isar: splitter support; improved diagnostics;
tuned;
NEWS
     1.1 --- a/NEWS	Thu Mar 16 00:29:03 2000 +0100
     1.2 +++ b/NEWS	Thu Mar 16 00:31:58 2000 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4  * ML: PureThy.add_thms/add_axioms/add_defs now return theorems;
     1.5  
     1.6  
     1.7 -*** Isabelle document preparation ***
     1.8 +*** Document preparation ***
     1.9  
    1.10  * isatool mkdir provides easy setup of Isabelle session directories,
    1.11  including proper documents;
    1.12 @@ -35,11 +35,15 @@
    1.13  * Pure: new 'obtain' language element supports generalized existence
    1.14  proofs;
    1.15  
    1.16 -* Pure: much better support for case-analysis type proofs: new 'case'
    1.17 +* Pure: scalable support for case-analysis type proofs: new 'case'
    1.18  language element refers to local contexts symbolically, as produced by
    1.19  certain proof methods; internally, case names are attached to theorems
    1.20  as "tags";
    1.21  
    1.22 +* Provers: splitter support (via 'split' attribute and 'simp' method
    1.23 +modifier); 'simp' method: 'only:' modifier removes loopers as well
    1.24 +(including splits);
    1.25 +
    1.26  * HOL: new proof method 'cases' and improved version of 'induct' now
    1.27  support named cases; major packages (inductive, datatype, primrec,
    1.28  recdef) support case names and properly name parameters;
    1.29 @@ -51,6 +55,12 @@
    1.30  
    1.31  * intro/elim/dest attributes: changed ! / !! flags to ? / ??;
    1.32  
    1.33 +* 'pr' command: optional goals_limit argument;
    1.34 +
    1.35 +* diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit
    1.36 +additional print modes to be specified; e.g. pr(latex) will print
    1.37 +proof according to the Isabelle LaTeX style;
    1.38 +
    1.39  
    1.40  *** HOL ***
    1.41