changeset 12034 | 4471077c4d4f |
parent 12022 | 9c3377b133c0 |
child 12078 | 4eb8061286e5 |
--- 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 ***