# HG changeset patch
# User wenzelm
# Date 1004809221 -3600
# Node ID 4471077c4d4fb4a6d05b0c19c0b01f3fc9efec42
# Parent  69cb2059aadc184ed53219b92288df25b8babd3b
* 'domain' package adapted to new-style theories, e.g. see
HOLCF/ex/Dnat.thy;

diff -r 69cb2059aadc -r 4471077c4d4f NEWS
--- a/NEWS	Sat Nov 03 01:45:32 2001 +0100
+++ b/NEWS	Sat Nov 03 18:40:21 2001 +0100
@@ -170,7 +170,10 @@
 *** HOLCF ***
 
 * proper rep_datatype lift (see theory Lift); use plain induct_tac
-instead of lift.induct_tac, use UU instead of Undef in all cases;
+instead of former lift.induct_tac; always use UU instead of Undef;
+
+* 'domain' package adapted to new-style theories, e.g. see
+HOLCF/ex/Dnat.thy;
 
 
 *** ZF ***