src/HOL/Induct/Mutil.thy
changeset 11464 ddea204de5bc
parent 11046 b5f5942781a0
child 11637 647e6c84323c
     1.1 --- a/src/HOL/Induct/Mutil.thy	Mon Aug 06 13:12:06 2001 +0200
     1.2 +++ b/src/HOL/Induct/Mutil.thy	Mon Aug 06 13:43:24 2001 +0200
     1.3 @@ -110,7 +110,7 @@
     1.4    Diff_Int_distrib [simp]
     1.5  
     1.6  lemma tiling_domino_0_1:
     1.7 -  "t \<in> tiling domino ==> card (coloured 0 \<inter> t) = card (coloured 1 \<inter> t)"
     1.8 +  "t \<in> tiling domino ==> card (coloured 0 \<inter> t) = card (coloured 1' \<inter> t)"
     1.9    apply (erule tiling.induct)
    1.10     apply (drule_tac [2] domino_singletons)
    1.11     apply auto
    1.12 @@ -131,7 +131,7 @@
    1.13    apply (rule notI)
    1.14    apply (subgoal_tac
    1.15      "card (coloured 0 \<inter> (t - {(i, j)} - {(m, n)})) <
    1.16 -      card (coloured 1 \<inter> (t - {(i, j)} - {(m, n)}))")
    1.17 +      card (coloured 1' \<inter> (t - {(i, j)} - {(m, n)}))")
    1.18     apply (force simp only: tiling_domino_0_1)
    1.19    apply (simp add: tiling_domino_0_1 [symmetric])
    1.20    apply (simp add: coloured_def card_Diff2_less)