diff -r 4e9df6ffcc6e -r e4b69e10b990 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Thu May 24 17:05:30 2012 +0200
+++ b/src/HOL/Set_Interval.thy	Thu May 24 17:25:53 2012 +0200
@@ -831,7 +831,7 @@
   done
 
 lemma finite_atLeastZeroLessThan_int: "finite {(0::int)..<u}"
-  apply (case_tac "0 \<le> u")
+  apply (cases "0 \<le> u")
   apply (subst image_atLeastZeroLessThan_int, assumption)
   apply (rule finite_imageI)
   apply auto
@@ -858,7 +858,7 @@
 subsubsection {* Cardinality *}
 
 lemma card_atLeastZeroLessThan_int: "card {(0::int)..<u} = nat u"
-  apply (case_tac "0 \<le> u")
+  apply (cases "0 \<le> u")
   apply (subst image_atLeastZeroLessThan_int, assumption)
   apply (subst card_image)
   apply (auto simp add: inj_on_def)