# HG changeset patch
# User wenzelm
# Date 925721834 -7200
# Node ID 128cf997c768638a88ac598ddf2584df3b024dd0
# Parent  ac091e18b9fc27ea8c755efc7f0f08bf78d5793c
tuned;

diff -r ac091e18b9fc -r 128cf997c768 NEWS
--- 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 ***