src/HOL/Integration.thy
changeset 30082 43c5b7bfc791
parent 29833 409138c4de12
child 31252 5155117f9d66
     1.1 --- a/src/HOL/Integration.thy	Tue Feb 24 11:10:05 2009 -0800
     1.2 +++ b/src/HOL/Integration.thy	Tue Feb 24 11:12:58 2009 -0800
     1.3 @@ -134,7 +134,7 @@
     1.4  apply (frule partition [THEN iffD1], safe)
     1.5  apply (drule_tac x = "psize D" and P="%n. psize D \<le> n --> ?P n" in spec, safe)
     1.6  apply (case_tac "psize D = 0")
     1.7 -apply (drule_tac [2] n = "psize D - 1" in partition_lt, auto)
     1.8 +apply (drule_tac [2] n = "psize D - Suc 0" in partition_lt, auto)
     1.9  done
    1.10  
    1.11  lemma partition_gt: "[|partition(a,b) D; n < (psize D)|] ==> D(n) < D(psize D)"
    1.12 @@ -145,7 +145,7 @@
    1.13  apply (rotate_tac 2)
    1.14  apply (drule_tac x = "psize D" in spec)
    1.15  apply (rule ccontr)
    1.16 -apply (drule_tac n = "psize D - 1" in partition_lt)
    1.17 +apply (drule_tac n = "psize D - Suc 0" in partition_lt)
    1.18  apply auto
    1.19  done
    1.20