# HG changeset patch
# User paulson
# Date 904655159 -7200
# Node ID 3a744748dd21e02cc643ef154d264c39cd8f228d
# Parent  a895ab904b85ca7d48715892b93519e3246ec987
tidied

diff -r a895ab904b85 -r 3a744748dd21 src/HOL/Induct/Mutil.ML
--- a/src/HOL/Induct/Mutil.ML	Tue Sep 01 15:05:36 1998 +0200
+++ b/src/HOL/Induct/Mutil.ML	Tue Sep 01 15:05:59 1998 +0200
@@ -10,8 +10,7 @@
 
 (** The union of two disjoint tilings is a tiling **)
 
-Goal "t: tiling A ==> \
-\              u: tiling A --> t <= Compl u --> t Un u : tiling A";
+Goal "t: tiling A ==> u: tiling A --> t <= Compl u --> t Un u : tiling A";
 by (etac tiling.induct 1);
 by (Simp_tac 1);
 by (simp_tac (simpset() addsimps [Un_assoc]) 1);
@@ -141,8 +140,8 @@
 (*Final argument is surprisingly complex.  Note the use of small simpsets
   to avoid moving Sucs, etc.*)
 Goal "[| t = below(Suc m + Suc m) Times below(Suc n + Suc n);   \
-\                   t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))}              \
-\                |] ==> t' ~: tiling domino";
+\        t' = t - {(0,0)} - {(Suc(m+m), Suc(n+n))}              \
+\     |] ==> t' ~: tiling domino";
 by (rtac notI 1);
 by (subgoal_tac "card(evnodd t' 0) < card(evnodd t' 1)" 1);
 by (asm_full_simp_tac (HOL_ss addsimps [less_not_refl, tiling_domino_0_1]) 1);