src/HOL/SPARK/SPARK.thy

       case 0
       with 3 have "bin BIT bit = 0" by simp
       then have "bin = 0" "bit = 0"
         by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
       then show ?thesis using 0 1 `y < 2 ^ n`
-        by simp (simp add: Bit0_def int_or_Pls [unfolded Pls_def])
+        by simp
     next
       case (Suc m)
       from 3 have "0 \<le> bin"
         by (simp add: Bit_def bitval_def split add: bit.split_asm)
       moreover from 3 Suc have "bin < 2 ^ m"

       case 0
       with 3 have "bin BIT bit = 0" by simp
       then have "bin = 0" "bit = 0"
         by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
       then show ?thesis using 0 1 `y < 2 ^ n`
-        by simp (simp add: Bit0_def int_xor_Pls [unfolded Pls_def])
+        by simp
     next
       case (Suc m)
       from 3 have "0 \<le> bin"
         by (simp add: Bit_def bitval_def split add: bit.split_asm)
       moreover from 3 Suc have "bin < 2 ^ m"

   fixes x :: int
   shows "x AND 2 ^ n - 1 = x mod 2 ^ n"
 proof (induct x arbitrary: n rule: bin_induct)
   case 1
   then show ?case
-    by simp (simp add: Pls_def)
+    by simp
 next
   case 2
   then show ?case
-    by (simp, simp only: Min_def, simp add: m1mod2k)
+    by (simp, simp add: m1mod2k)
 next
   case (3 bin bit)
   show ?case
   proof (cases n)
     case 0
-    then show ?thesis by (simp add: int_and_extra_simps [unfolded Pls_def])
+    then show ?thesis by (simp add: int_and_extra_simps)
   next
     case (Suc m)
     with 3 show ?thesis
       by (simp only: power_BIT mod_BIT int_and_Bits) simp
   qed