# HG changeset patch
# User paulson
# Date 864732300 -7200
# Node ID c224dddc5f71c6e0bbd7eb34412cef6c3d313fc8
# Parent  9b899eb8a0361d11195230cce4183d28d8d12b31
Removal of card_insert_disjoint, which is now a default rewrite rule

diff -r 9b899eb8a036 -r c224dddc5f71 src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Tue May 27 13:24:15 1997 +0200
+++ b/src/HOL/Induct/Mutil.ML	Tue May 27 13:25:00 1997 +0200
@@ -141,8 +141,7 @@
 by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
 by (asm_simp_tac (!simpset addsimps [evnodd_Un, Un_insert_left, 
                                      tiling_domino_finite,
-                                     evnodd_subset RS finite_subset,
-                                     card_insert_disjoint]) 1);
+                                     evnodd_subset RS finite_subset]) 1);
 by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
 qed "tiling_domino_0_1";