* 'domain' package adapted to new-style theories, e.g. see
authorwenzelm
Sat, 03 Nov 2001 18:40:21 +0100
changeset 120344471077c4d4f
parent 12033 69cb2059aadc
child 12035 f2ee4b5d02f2
* 'domain' package adapted to new-style theories, e.g. see
HOLCF/ex/Dnat.thy;
NEWS
     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 ***