* 'domain' package adapted to new-style theories, e.g. see
HOLCF/ex/Dnat.thy;
1.1 --- a/NEWS Sat Nov 03 01:45:32 2001 +0100
1.2 +++ b/NEWS Sat Nov 03 18:40:21 2001 +0100
1.3 @@ -170,7 +170,10 @@
1.4 *** HOLCF ***
1.5
1.6 * proper rep_datatype lift (see theory Lift); use plain induct_tac
1.7 -instead of lift.induct_tac, use UU instead of Undef in all cases;
1.8 +instead of former lift.induct_tac; always use UU instead of Undef;
1.9 +
1.10 +* 'domain' package adapted to new-style theories, e.g. see
1.11 +HOLCF/ex/Dnat.thy;
1.12
1.13
1.14 *** ZF ***