# HG changeset patch # User wenzelm # Date 1028625867 -7200 # Node ID 07747943c62651edec79d7b117c68491b7df202c # Parent 56610e2ba220d62841e1f2f0de8ba71e2d885d61 * Provers: Simplifier.simproc(_i) now provide sane interface for setting up simprocs; diff -r 56610e2ba220 -r 07747943c626 NEWS --- a/NEWS Tue Aug 06 11:22:05 2002 +0200 +++ b/NEWS Tue Aug 06 11:24:27 2002 +0200 @@ -19,15 +19,18 @@ parameters (as in CASL, for example); just specify something like ``var x + var y + struct M'' as import; -* improved induct method: assumptions introduced by case "foo" are -split into "foo.hyps" (from the rule) and "foo.prems" (from the goal -statement); "foo" still refers to all facts collectively; - -* improved thms_containing: proper indexing of facts instead of raw -theorems; check validity of results wrt. current name space; include -local facts of proof configuration (also covers active locales); an -optional limit for the number of printed facts may be given (the -default is 40); +* Pure: improved thms_containing: proper indexing of facts instead of +raw theorems; check validity of results wrt. current name space; +include local facts of proof configuration (also covers active +locales); an optional limit for the number of printed facts may be +given (the default is 40); + +* Provers: improved induct method: assumptions introduced by case +"foo" are split into "foo.hyps" (from the rule) and "foo.prems" (from +the goal statement); "foo" still refers to all facts collectively; + +* Provers: Simplifier.simproc(_i) now provide sane interface for +setting up simprocs; *** HOL ***