# HG changeset patch
# User paulson
# Date 828095927 -3600
# Node ID 8c84606672fe922825e001be2025b3b932806279
# Parent  b5e43a60443aaecb6bfa133c193dffcce3944610
Simplified proof of tiling_UnI

diff -r b5e43a60443a -r 8c84606672fe src/ZF/ex/Mutil.ML
--- a/src/ZF/ex/Mutil.ML	Fri Mar 29 10:54:44 1996 +0100
+++ b/src/ZF/ex/Mutil.ML	Fri Mar 29 11:38:47 1996 +0100
@@ -67,22 +67,13 @@
 (** The union of two disjoint tilings is a tiling **)
 
 goal thy "!!t. t: tiling(A) ==> \
-\              ALL u: tiling(A). t Int u = 0 --> t Un u : tiling(A)";
+\              u: tiling(A) --> t Int u = 0 --> t Un u : tiling(A)";
 by (etac tiling.induct 1);
 by (simp_tac (ZF_ss addsimps tiling.intrs) 1);
-by (asm_full_simp_tac (ZF_ss addsimps [Int_Un_distrib, Un_assoc, Un_subset_iff,
-				       subset_empty_iff RS iff_sym]) 1);
-by (safe_tac ZF_cs);
-by (resolve_tac tiling.intrs 1);
-by (assume_tac 1);
-by (fast_tac ZF_cs 1);
-by (fast_tac eq_cs 1);
-val lemma = result();
-
-goal thy "!!t u. [| t: tiling(A);  u: tiling(A);  t Int u = 0 |] ==> \
-\                t Un u : tiling(A)";
-by (fast_tac (ZF_cs addIs [lemma RS bspec RS mp]) 1);
-qed "tiling_UnI";
+by (fast_tac (ZF_cs addIs tiling.intrs
+	             addss (ZF_ss addsimps [Un_assoc,
+					    subset_empty_iff RS iff_sym])) 1);
+bind_thm ("tiling_UnI", result() RS mp RS mp);
 
 goal thy "!!t. t:tiling(domino) ==> Finite(t)";
 by (eresolve_tac [tiling.induct] 1);