src/HOL/Set_Interval.thy
changeset 47988 e4b69e10b990
parent 47317 432b29a96f61
child 50417 f18b92f91818
     1.1 --- a/src/HOL/Set_Interval.thy	Thu May 24 17:05:30 2012 +0200
     1.2 +++ b/src/HOL/Set_Interval.thy	Thu May 24 17:25:53 2012 +0200
     1.3 @@ -831,7 +831,7 @@
     1.4    done
     1.5  
     1.6  lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}"
     1.7 -  apply (case_tac "0 \<le> u")
     1.8 +  apply (cases "0 \<le> u")
     1.9    apply (subst image_atLeastZeroLessThan_int, assumption)
    1.10    apply (rule finite_imageI)
    1.11    apply auto
    1.12 @@ -858,7 +858,7 @@
    1.13  subsubsection {* Cardinality *}
    1.14  
    1.15  lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u"
    1.16 -  apply (case_tac "0 \<le> u")
    1.17 +  apply (cases "0 \<le> u")
    1.18    apply (subst image_atLeastZeroLessThan_int, assumption)
    1.19    apply (subst card_image)
    1.20    apply (auto simp add: inj_on_def)