src/HOL/SetInterval.thy

   show "?A \<subseteq> ?B" by auto
 next
   show "?B \<subseteq> ?A"
   proof
     fix n assume a: "n : ?B"
-    hence "n - k : {i..j}" by auto arith+
+    hence "n - k : {i..j}" by auto
     moreover have "n = (n - k) + k" using a by auto
     ultimately show "n : ?A" by blast
   qed
 qed
 

   show "?A \<subseteq> ?B" by auto
 next
   show "?B \<subseteq> ?A"
   proof
     fix n assume a: "n : ?B"
-    hence "n - k : {i..<j}" by auto arith+
+    hence "n - k : {i..<j}" by auto
     moreover have "n = (n - k) + k" using a by auto
     ultimately show "n : ?A" by blast
   qed
 qed
 

   apply (subgoal_tac "(%x. x + l) ` {..<u-l} = {l..<u}")
   apply (erule subst)
   apply (rule card_image)
   apply (simp add: inj_on_def)
   apply (auto simp add: image_def atLeastLessThan_def lessThan_def)
-  apply arith
   apply (rule_tac x = "x - l" in exI)
   apply arith
   done
 
 lemma card_atLeastAtMost [simp]: "card {l..u} = Suc u - l"