# HG changeset patch # User wenzelm # Date 953163118 -3600 # Node ID 5f3b0e02ec153b33a204778423e45ebae20d475a # Parent 85f504900ed5e9eb98fcd05abd8322ca305fd8be Isar: splitter support; improved diagnostics; tuned; diff -r 85f504900ed5 -r 5f3b0e02ec15 NEWS --- a/NEWS Thu Mar 16 00:29:03 2000 +0100 +++ b/NEWS Thu Mar 16 00:31:58 2000 +0100 @@ -14,7 +14,7 @@ * ML: PureThy.add_thms/add_axioms/add_defs now return theorems; -*** Isabelle document preparation *** +*** Document preparation *** * isatool mkdir provides easy setup of Isabelle session directories, including proper documents; @@ -35,11 +35,15 @@ * Pure: new 'obtain' language element supports generalized existence proofs; -* Pure: much better support for case-analysis type proofs: new 'case' +* Pure: scalable support for case-analysis type proofs: new 'case' language element refers to local contexts symbolically, as produced by certain proof methods; internally, case names are attached to theorems as "tags"; +* Provers: splitter support (via 'split' attribute and 'simp' method +modifier); 'simp' method: 'only:' modifier removes loopers as well +(including splits); + * HOL: new proof method 'cases' and improved version of 'induct' now support named cases; major packages (inductive, datatype, primrec, recdef) support case names and properly name parameters; @@ -51,6 +55,12 @@ * intro/elim/dest attributes: changed ! / !! flags to ? / ??; +* 'pr' command: optional goals_limit argument; + +* diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit +additional print modes to be specified; e.g. pr(latex) will print +proof according to the Isabelle LaTeX style; + *** HOL ***