src/HOL/Datatype.thy
changeset 14208 144f45277d5a
parent 14187 26dfcd0ac436
child 14274 0cb8a9a144d2
     1.1 --- a/src/HOL/Datatype.thy	Fri Sep 26 10:34:28 2003 +0200
     1.2 +++ b/src/HOL/Datatype.thy	Fri Sep 26 10:34:57 2003 +0200
     1.3 @@ -55,11 +55,9 @@
     1.4    show P
     1.5      apply (rule r)
     1.6       apply (rule ext)
     1.7 -     apply (cut_tac x = "Inl x" in a [THEN fun_cong])
     1.8 -     apply simp
     1.9 +     apply (cut_tac x = "Inl x" in a [THEN fun_cong], simp)
    1.10      apply (rule ext)
    1.11 -    apply (cut_tac x = "Inr x" in a [THEN fun_cong])
    1.12 -    apply simp
    1.13 +    apply (cut_tac x = "Inr x" in a [THEN fun_cong], simp)
    1.14      done
    1.15  qed
    1.16  
    1.17 @@ -89,8 +87,7 @@
    1.18  lemma prod_cases3 [case_names fields, cases type]:
    1.19      "(!!a b c. y = (a, b, c) ==> P) ==> P"
    1.20    apply (cases y)
    1.21 -  apply (case_tac b)
    1.22 -  apply blast
    1.23 +  apply (case_tac b, blast)
    1.24    done
    1.25  
    1.26  lemma prod_induct3 [case_names fields, induct type]:
    1.27 @@ -100,8 +97,7 @@
    1.28  lemma prod_cases4 [case_names fields, cases type]:
    1.29      "(!!a b c d. y = (a, b, c, d) ==> P) ==> P"
    1.30    apply (cases y)
    1.31 -  apply (case_tac c)
    1.32 -  apply blast
    1.33 +  apply (case_tac c, blast)
    1.34    done
    1.35  
    1.36  lemma prod_induct4 [case_names fields, induct type]:
    1.37 @@ -111,8 +107,7 @@
    1.38  lemma prod_cases5 [case_names fields, cases type]:
    1.39      "(!!a b c d e. y = (a, b, c, d, e) ==> P) ==> P"
    1.40    apply (cases y)
    1.41 -  apply (case_tac d)
    1.42 -  apply blast
    1.43 +  apply (case_tac d, blast)
    1.44    done
    1.45  
    1.46  lemma prod_induct5 [case_names fields, induct type]:
    1.47 @@ -122,8 +117,7 @@
    1.48  lemma prod_cases6 [case_names fields, cases type]:
    1.49      "(!!a b c d e f. y = (a, b, c, d, e, f) ==> P) ==> P"
    1.50    apply (cases y)
    1.51 -  apply (case_tac e)
    1.52 -  apply blast
    1.53 +  apply (case_tac e, blast)
    1.54    done
    1.55  
    1.56  lemma prod_induct6 [case_names fields, induct type]:
    1.57 @@ -133,8 +127,7 @@
    1.58  lemma prod_cases7 [case_names fields, cases type]:
    1.59      "(!!a b c d e f g. y = (a, b, c, d, e, f, g) ==> P) ==> P"
    1.60    apply (cases y)
    1.61 -  apply (case_tac f)
    1.62 -  apply blast
    1.63 +  apply (case_tac f, blast)
    1.64    done
    1.65  
    1.66  lemma prod_induct7 [case_names fields, induct type]: