record_simproc;
authorwenzelm
Mon Aug 23 16:50:10 1999 +0200 (1999-08-23)
changeset 7326a1555491a966
parent 7325 01bb8abb5a91
child 7327 596318fdb379
record_simproc;
NEWS
     1.1 --- a/NEWS	Mon Aug 23 16:38:29 1999 +0200
     1.2 +++ b/NEWS	Mon Aug 23 16:50:10 1999 +0200
     1.3 @@ -161,6 +161,15 @@
     1.4  
     1.5    datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
     1.6  
     1.7 +* HOL/record: record_simproc (part of the default simpset) takes care
     1.8 +of selectors applied to updated records; record_split_tac is no longer
     1.9 +part of the default claset; COMPATIBILITY:
    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