src/HOL/SPARK/SPARK.thy
changeset 47108 2a1953f0d20d
parent 41561 d1318f3c86ba
child 50788 fec14e8fefb8
     1.1 --- a/src/HOL/SPARK/SPARK.thy	Sat Mar 24 16:27:04 2012 +0100
     1.2 +++ b/src/HOL/SPARK/SPARK.thy	Sun Mar 25 20:15:39 2012 +0200
     1.3 @@ -145,7 +145,7 @@
     1.4        then have "bin = 0" "bit = 0"
     1.5          by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
     1.6        then show ?thesis using 0 1 `y < 2 ^ n`
     1.7 -        by simp (simp add: Bit0_def int_or_Pls [unfolded Pls_def])
     1.8 +        by simp
     1.9      next
    1.10        case (Suc m)
    1.11        from 3 have "0 \<le> bin"
    1.12 @@ -188,7 +188,7 @@
    1.13        then have "bin = 0" "bit = 0"
    1.14          by (auto simp add: Bit_def bitval_def split add: bit.split_asm) arith
    1.15        then show ?thesis using 0 1 `y < 2 ^ n`
    1.16 -        by simp (simp add: Bit0_def int_xor_Pls [unfolded Pls_def])
    1.17 +        by simp
    1.18      next
    1.19        case (Suc m)
    1.20        from 3 have "0 \<le> bin"
    1.21 @@ -257,17 +257,17 @@
    1.22  proof (induct x arbitrary: n rule: bin_induct)
    1.23    case 1
    1.24    then show ?case
    1.25 -    by simp (simp add: Pls_def)
    1.26 +    by simp
    1.27  next
    1.28    case 2
    1.29    then show ?case
    1.30 -    by (simp, simp only: Min_def, simp add: m1mod2k)
    1.31 +    by (simp, simp add: m1mod2k)
    1.32  next
    1.33    case (3 bin bit)
    1.34    show ?case
    1.35    proof (cases n)
    1.36      case 0
    1.37 -    then show ?thesis by (simp add: int_and_extra_simps [unfolded Pls_def])
    1.38 +    then show ?thesis by (simp add: int_and_extra_simps)
    1.39    next
    1.40      case (Suc m)
    1.41      with 3 show ?thesis