NEWS
changeset 6563 128cf997c768
parent 6533 b8929d23aaa4
child 6671 677713791bd8
--- a/NEWS	Mon May 03 10:51:44 1999 +0200
+++ b/NEWS	Mon May 03 10:57:14 1999 +0200
@@ -72,8 +72,6 @@
 
 *** HOL ***
 
-* recdef (TFL) now requires theory Recdef;
-
 * There are now decision procedures for linear arithmetic over nat and
 int:
 
@@ -107,6 +105,8 @@
 * HOL/typedef: fixed type inference for representing set; type
 arguments now have to occur explicitly on the rhs as type constraints;
 
+* HOL/recdef (TFL) now requires theory Recdef;
+
 
 *** ZF ***