# HG changeset patch
# User paulson
# Date 838045487 -7200
# Node ID 83c70ad381c14504b2354478faa79dd8fbca77f0
# Parent  ac8e534b48341fdb08ca75d752bde0d2cbad4e5b
Added insert_commute

diff -r ac8e534b4834 -r 83c70ad381c1 src/HOL/equalities.ML
--- a/src/HOL/equalities.ML	Mon Jul 22 16:16:51 1996 +0200
+++ b/src/HOL/equalities.ML	Mon Jul 22 16:24:47 1996 +0200
@@ -58,6 +58,10 @@
 qed "insert_absorb2";
 Addsimps [insert_absorb2];
 
+goal Set.thy "insert x (insert y A) = insert y (insert x A)";
+by (Fast_tac 1);
+qed "insert_commute";
+
 goal Set.thy "(insert x A <= B) = (x:B & A <= B)";
 by (Fast_tac 1);
 qed "insert_subset";