* Pure: disallow duplicate fact bindings within new-style theory files;
authorwenzelm
Tue, 27 Aug 2002 16:41:52 +0200
changeset 13540 aede0306e214
parent 13539 7d62554fa0e0
child 13541 44efea0e21fa
* Pure: disallow duplicate fact bindings within new-style theory files;
NEWS
--- 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;