tuned;
authorwenzelm
Mon Aug 23 16:51:48 1999 +0200 (1999-08-23)
changeset 7327596318fdb379
parent 7326 a1555491a966
child 7328 4265615b4206
tuned;
NEWS
     1.1 --- a/NEWS	Mon Aug 23 16:50:10 1999 +0200
     1.2 +++ b/NEWS	Mon Aug 23 16:51:48 1999 +0200
     1.3 @@ -163,13 +163,12 @@
     1.4  
     1.5  * HOL/record: record_simproc (part of the default simpset) takes care
     1.6  of selectors applied to updated records; record_split_tac is no longer
     1.7 -part of the default claset; COMPATIBILITY:
     1.8 +part of the default claset; update_defs may now be removed from the
     1.9 +simpset in many cases; COMPATIBILITY: old behavior achieved by
    1.10  
    1.11    claset_ref () := claset() addSWrapper record_split_wrapper;
    1.12    Delsimprocs [record_simproc]
    1.13  
    1.14 -achieve the old bahaviour;
    1.15 -
    1.16  * HOL/typedef: fixed type inference for representing set; type
    1.17  arguments now have to occur explicitly on the rhs as type constraints;
    1.18