author | wenzelm |
Mon, 03 May 1999 10:57:14 +0200 | |
changeset 6563 | 128cf997c768 |
parent 6562 | ac091e18b9fc |
child 6564 | c09997086ca7 |
--- 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 ***