author | wenzelm |
Tue, 27 Aug 2002 16:41:52 +0200 | |
changeset 13540 | aede0306e214 |
parent 13539 | 7d62554fa0e0 |
child 13541 | 44efea0e21fa |
--- a/NEWS Tue Aug 27 16:41:01 2002 +0200 +++ b/NEWS Tue Aug 27 16:41:52 2002 +0200 @@ -25,6 +25,9 @@ locales); an optional limit for the number of printed facts may be given (the default is 40); +* Pure: disallow duplicate fact bindings within new-style theory +files; + * 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;