diff -r f30b73385060 -r 25b068a99d2b src/HOL/NumberTheory/Finite2.thy
--- a/src/HOL/NumberTheory/Finite2.thy	Wed Jul 26 13:31:07 2006 +0200
+++ b/src/HOL/NumberTheory/Finite2.thy	Wed Jul 26 19:23:04 2006 +0200
@@ -179,10 +179,6 @@
 lemma int_card_bdd_int_set_l_l: "0 < n ==>
     int(card {x. 0 < x & x < n}) = n - 1"
   apply (auto simp add: card_bdd_int_set_l_l)
-  apply (subgoal_tac "Suc 0 \<le> nat n")
-   apply (auto simp add: zdiff_int [symmetric])
-  apply (subgoal_tac "0 < nat n", arith)
-  apply (simp add: zero_less_nat_eq)
   done
 
 lemma int_card_bdd_int_set_l_le: "0 \<le> n ==>