src/HOL/SetInterval.thy
changeset 29920 b95f5b8b93dd
parent 29709 cf8476cc440d
child 29960 9d5c6f376768
child 30240 5b25fee0362c
     1.1 --- a/src/HOL/SetInterval.thy	Sun Feb 15 07:54:46 2009 +0100
     1.2 +++ b/src/HOL/SetInterval.thy	Sun Feb 15 11:26:38 2009 +0100
     1.3 @@ -568,7 +568,6 @@
     1.4  apply auto
     1.5  apply (case_tac xa)
     1.6  apply auto
     1.7 -apply (auto simp add: finite_M_bounded_by_nat)
     1.8  done
     1.9  
    1.10  lemma card_less_Suc: