# HG changeset patch
# User paulson
# Date 865246455 -7200
# Node ID 5ef99c94e1fbef0ed140eb443d07faf0416ddcc8
# Parent  7707cb7a50546ddebddab7c1ca14ea381bab1a54
Now Un_insert_left, Un_insert_right are default rewrite rules

diff -r 7707cb7a5054 -r 5ef99c94e1fb src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Mon Jun 02 12:13:42 1997 +0200
+++ b/src/HOL/equalities.ML	Mon Jun 02 12:14:15 1997 +0200
@@ -228,10 +228,12 @@
 goal Set.thy "(insert a B) Un C = insert a (B Un C)";
 by (Blast_tac 1);
 qed "Un_insert_left";
+Addsimps[Un_insert_left];
 
 goal Set.thy "A Un (insert a B) = insert a (A Un B)";
 by (Blast_tac 1);
 qed "Un_insert_right";
+Addsimps[Un_insert_right];
 
 goal Set.thy "(insert a B) Int C = (if a:C then insert a (B Int C) \
 \                                          else        B Int C)";