src/HOL/Statespace/DistinctTreeProver.thy
changeset 44890 22f665a2e91c
parent 42287 d98eb048a2e4
child 45355 c0704e988526
     1.1 --- a/src/HOL/Statespace/DistinctTreeProver.thy	Sun Sep 11 22:56:05 2011 +0200
     1.2 +++ b/src/HOL/Statespace/DistinctTreeProver.thy	Mon Sep 12 07:55:43 2011 +0200
     1.3 @@ -141,7 +141,7 @@
     1.4        case None
     1.5        with l'_l Some x_l_Some del
     1.6        show ?thesis
     1.7 -        by (fastsimp split: split_if_asm)
     1.8 +        by (fastforce split: split_if_asm)
     1.9      qed
    1.10    next
    1.11      case None
    1.12 @@ -154,12 +154,12 @@
    1.13          by simp
    1.14        with Some x_l_None del
    1.15        show ?thesis
    1.16 -        by (fastsimp split: split_if_asm)
    1.17 +        by (fastforce split: split_if_asm)
    1.18      next
    1.19        case None
    1.20        with x_l_None del
    1.21        show ?thesis
    1.22 -        by (fastsimp split: split_if_asm)
    1.23 +        by (fastforce split: split_if_asm)
    1.24      qed
    1.25    qed
    1.26  qed
    1.27 @@ -198,12 +198,12 @@
    1.28        
    1.29        with dist_l' dist_r' l'_l Some x_l_Some del d dist_l_r
    1.30        show ?thesis
    1.31 -        by fastsimp
    1.32 +        by fastforce
    1.33      next
    1.34        case None
    1.35        with l'_l dist_l'  x_l_Some del d dist_l_r dist_r
    1.36        show ?thesis
    1.37 -        by fastsimp
    1.38 +        by fastforce
    1.39      qed
    1.40    next
    1.41      case None
    1.42 @@ -218,12 +218,12 @@
    1.43        have "set_of r' \<subseteq> set_of r".
    1.44        with Some dist_r' x_l_None del dist_l d dist_l_r
    1.45        show ?thesis
    1.46 -        by fastsimp
    1.47 +        by fastforce
    1.48      next
    1.49        case None
    1.50        with x_l_None del dist_l dist_r d dist_l_r
    1.51        show ?thesis
    1.52 -        by (fastsimp split: split_if_asm)
    1.53 +        by (fastforce split: split_if_asm)
    1.54      qed
    1.55    qed
    1.56  qed