# HG changeset patch
# User wenzelm
# Date 935419810 -7200
# Node ID a1555491a96676c65ba4e8931c2fe222b81b2ede
# Parent  01bb8abb5a91063233291fe456fb4b8dab941b14
record_simproc;

diff -r 01bb8abb5a91 -r a1555491a966 NEWS
--- a/NEWS	Mon Aug 23 16:38:29 1999 +0200
+++ b/NEWS	Mon Aug 23 16:50:10 1999 +0200
@@ -161,6 +161,15 @@
 
   datatype 'a tree = Atom 'a | Branch "nat => 'a tree"
 
+* HOL/record: record_simproc (part of the default simpset) takes care
+of selectors applied to updated records; record_split_tac is no longer
+part of the default claset; COMPATIBILITY:
+
+  claset_ref () := claset() addSWrapper record_split_wrapper;
+  Delsimprocs [record_simproc]
+
+achieve the old bahaviour;
+
 * HOL/typedef: fixed type inference for representing set; type
 arguments now have to occur explicitly on the rhs as type constraints;