corrected and unified thm names
authornipkow
Wed Jun 24 09:41:14 2009 +0200 (2009-06-24)
changeset 3179005c92381363c
parent 31789 c8a590599cb5
child 31791 c9a1caf218c8
corrected and unified thm names
NEWS
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Decision_Procs/cooper_tac.ML
src/HOL/Decision_Procs/ferrack_tac.ML
src/HOL/Decision_Procs/mir_tac.ML
src/HOL/Groebner_Basis.thy
src/HOL/Import/HOL/arithmetic.imp
src/HOL/Library/Formal_Power_Series.thy
src/HOL/MetisExamples/BT.thy
src/HOL/Nat_Numeral.thy
src/HOL/Presburger.thy
src/HOL/Tools/Groebner_Basis/normalizer.ML
src/HOL/Tools/Qelim/presburger.ML
src/HOL/Tools/nat_numeral_simprocs.ML
src/HOL/Transcendental.thy
src/HOL/Word/BinBoolList.thy
     1.1 --- a/NEWS	Tue Jun 23 21:07:39 2009 +0200
     1.2 +++ b/NEWS	Wed Jun 24 09:41:14 2009 +0200
     1.3 @@ -43,6 +43,11 @@
     1.4  * Constants Set.Pow and Set.image now with authentic syntax; object-logic definitions
     1.5  Set.Pow_def and Set.image_def.  INCOMPATIBILITY.
     1.6  
     1.7 +* Renamed theorems:
     1.8 +Suc_eq_add_numeral_1 -> Suc_eq_plus1
     1.9 +Suc_eq_add_numeral_1_left -> Suc_eq_plus1_left
    1.10 +Suc_plus1 -> Suc_eq_plus1
    1.11 +
    1.12  * Discontinued ancient tradition to suffix certain ML module names with "_package", e.g.:
    1.13  
    1.14      DatatypePackage ~> Datatype
     2.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Tue Jun 23 21:07:39 2009 +0200
     2.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Wed Jun 24 09:41:14 2009 +0200
     2.3 @@ -422,7 +422,7 @@
     2.4  
     2.5      have "\<bar> real x \<bar> \<le> 1"  using `0 \<le> real x` `real x \<le> 1` by auto
     2.6      from mp[OF summable_Leibniz(2)[OF zeroseq_arctan_series[OF this] monoseq_arctan_series[OF this]] prem, THEN spec, of m, unfolded `2 * m = n`]
     2.7 -    show ?thesis unfolding arctan_series[OF `\<bar> real x \<bar> \<le> 1`] Suc_plus1  .
     2.8 +    show ?thesis unfolding arctan_series[OF `\<bar> real x \<bar> \<le> 1`] Suc_eq_plus1  .
     2.9    qed auto
    2.10    note arctan_bounds = this[unfolded atLeastAtMost_iff]
    2.11  
    2.12 @@ -1179,7 +1179,7 @@
    2.13  proof (induct n arbitrary: x)
    2.14    case (Suc n)
    2.15    have split_pi_off: "x + real (Suc n) * 2 * pi = (x + real n * 2 * pi) + 2 * pi"
    2.16 -    unfolding Suc_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
    2.17 +    unfolding Suc_eq_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
    2.18    show ?case unfolding split_pi_off using Suc by auto
    2.19  qed auto
    2.20  
    2.21 @@ -1676,7 +1676,7 @@
    2.22      using ln_series[of "x + 1"] `0 \<le> x` `x < 1` by auto
    2.23  
    2.24    have "norm x < 1" using assms by auto
    2.25 -  have "?a ----> 0" unfolding Suc_plus1[symmetric] inverse_eq_divide[symmetric] 
    2.26 +  have "?a ----> 0" unfolding Suc_eq_plus1[symmetric] inverse_eq_divide[symmetric] 
    2.27      using LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_Suc[OF LIMSEQ_power_zero[OF `norm x < 1`]]] by auto
    2.28    { fix n have "0 \<le> ?a n" by (rule mult_nonneg_nonneg, auto intro!: mult_nonneg_nonneg simp add: `0 \<le> x`) }
    2.29    { fix n have "?a (Suc n) \<le> ?a n" unfolding inverse_eq_divide[symmetric]
     3.1 --- a/src/HOL/Decision_Procs/cooper_tac.ML	Tue Jun 23 21:07:39 2009 +0200
     3.2 +++ b/src/HOL/Decision_Procs/cooper_tac.ML	Wed Jun 24 09:41:14 2009 +0200
     3.3 @@ -31,7 +31,7 @@
     3.4  val split_zmod = @{thm split_zmod};
     3.5  val mod_div_equality' = @{thm mod_div_equality'};
     3.6  val split_div' = @{thm split_div'};
     3.7 -val Suc_plus1 = @{thm Suc_plus1};
     3.8 +val Suc_eq_plus1 = @{thm Suc_eq_plus1};
     3.9  val imp_le_cong = @{thm imp_le_cong};
    3.10  val conj_le_cong = @{thm conj_le_cong};
    3.11  val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
    3.12 @@ -81,11 +81,11 @@
    3.13  				  @{thm mod_by_0}, @{thm div_by_0},
    3.14  				  @{thm "zdiv_zero"}, @{thm "zmod_zero"}, @{thm "div_0"}, @{thm "mod_0"},
    3.15  				  @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
    3.16 -				  Suc_plus1]
    3.17 +				  Suc_eq_plus1]
    3.18  			addsimps @{thms add_ac}
    3.19  			addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
    3.20      val simpset0 = HOL_basic_ss
    3.21 -      addsimps [mod_div_equality', Suc_plus1]
    3.22 +      addsimps [mod_div_equality', Suc_eq_plus1]
    3.23        addsimps comp_arith
    3.24        addsplits [split_zdiv, split_zmod, split_div', @{thm "split_min"}, @{thm "split_max"}]
    3.25      (* Simp rules for changing (n::int) to int n *)
     4.1 --- a/src/HOL/Decision_Procs/ferrack_tac.ML	Tue Jun 23 21:07:39 2009 +0200
     4.2 +++ b/src/HOL/Decision_Procs/ferrack_tac.ML	Wed Jun 24 09:41:14 2009 +0200
     4.3 @@ -35,7 +35,7 @@
     4.4  val split_zmod = @{thm split_zmod};
     4.5  val mod_div_equality' = @{thm mod_div_equality'};
     4.6  val split_div' = @{thm split_div'};
     4.7 -val Suc_plus1 = @{thm Suc_plus1};
     4.8 +val Suc_eq_plus1 = @{thm Suc_eq_plus1};
     4.9  val imp_le_cong = @{thm imp_le_cong};
    4.10  val conj_le_cong = @{thm conj_le_cong};
    4.11  val mod_add_left_eq = @{thm mod_add_left_eq} RS sym;
     5.1 --- a/src/HOL/Decision_Procs/mir_tac.ML	Tue Jun 23 21:07:39 2009 +0200
     5.2 +++ b/src/HOL/Decision_Procs/mir_tac.ML	Wed Jun 24 09:41:14 2009 +0200
     5.3 @@ -26,7 +26,7 @@
     5.4  
     5.5    val comp_arith = (map thm ["Let_def", "if_False", "if_True", "add_0", 
     5.6                   "add_Suc", "add_number_of_left", "mult_number_of_left", 
     5.7 -                 "Suc_eq_add_numeral_1"])@
     5.8 +                 "Suc_eq_plus1"])@
     5.9                   (map (fn s => thm s RS sym) ["numeral_1_eq_1", "numeral_0_eq_0"])
    5.10                   @ @{thms arith_simps} @ nat_arith @ @{thms rel_simps} 
    5.11    val ths = [@{thm "mult_numeral_1"}, @{thm "mult_numeral_1_right"}, 
    5.12 @@ -50,7 +50,6 @@
    5.13  val split_zmod = @{thm "split_zmod"};
    5.14  val mod_div_equality' = @{thm "mod_div_equality'"};
    5.15  val split_div' = @{thm "split_div'"};
    5.16 -val Suc_plus1 = @{thm "Suc_plus1"};
    5.17  val imp_le_cong = @{thm "imp_le_cong"};
    5.18  val conj_le_cong = @{thm "conj_le_cong"};
    5.19  val mod_add_eq = @{thm "mod_add_eq"} RS sym;
    5.20 @@ -104,11 +103,11 @@
    5.21                                    @{thm "mod_self"}, @{thm "zmod_self"},
    5.22                                    @{thm "zdiv_zero"},@{thm "zmod_zero"},@{thm "div_0"}, @{thm "mod_0"},
    5.23                                    @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, @{thm "mod_1"},
    5.24 -                                  @{thm "Suc_plus1"}]
    5.25 +                                  @{thm "Suc_eq_plus1"}]
    5.26                          addsimps @{thms add_ac}
    5.27                          addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
    5.28      val simpset0 = HOL_basic_ss
    5.29 -      addsimps [mod_div_equality', Suc_plus1]
    5.30 +      addsimps [mod_div_equality', @{thm Suc_eq_plus1}]
    5.31        addsimps comp_ths
    5.32        addsplits [@{thm "split_zdiv"}, @{thm "split_zmod"}, @{thm "split_div'"}, @{thm "split_min"}, @{thm "split_max"}]
    5.33      (* Simp rules for changing (n::int) to int n *)
     6.1 --- a/src/HOL/Groebner_Basis.thy	Tue Jun 23 21:07:39 2009 +0200
     6.2 +++ b/src/HOL/Groebner_Basis.thy	Wed Jun 24 09:41:14 2009 +0200
     6.3 @@ -180,7 +180,7 @@
     6.4  lemmas comp_arith =
     6.5    Let_def arith_simps nat_arith rel_simps neg_simps if_False
     6.6    if_True add_0 add_Suc add_number_of_left mult_number_of_left
     6.7 -  numeral_1_eq_1[symmetric] Suc_eq_add_numeral_1
     6.8 +  numeral_1_eq_1[symmetric] Suc_eq_plus1
     6.9    numeral_0_eq_0[symmetric] numerals[symmetric]
    6.10    iszero_simps not_iszero_Numeral1
    6.11  
     7.1 --- a/src/HOL/Import/HOL/arithmetic.imp	Tue Jun 23 21:07:39 2009 +0200
     7.2 +++ b/src/HOL/Import/HOL/arithmetic.imp	Wed Jun 24 09:41:14 2009 +0200
     7.3 @@ -43,7 +43,7 @@
     7.4    "TWO" > "HOL4Base.arithmetic.TWO"
     7.5    "TIMES2" > "NatSimprocs.nat_mult_2"
     7.6    "SUC_SUB1" > "HOL4Base.arithmetic.SUC_SUB1"
     7.7 -  "SUC_ONE_ADD" > "Nat_Numeral.Suc_eq_add_numeral_1_left"
     7.8 +  "SUC_ONE_ADD" > "Nat_Numeral.Suc_eq_plus1_left"
     7.9    "SUC_NOT" > "Nat.nat.simps_2"
    7.10    "SUC_ELIM_THM" > "HOL4Base.arithmetic.SUC_ELIM_THM"
    7.11    "SUC_ADD_SYM" > "HOL4Base.arithmetic.SUC_ADD_SYM"
    7.12 @@ -265,7 +265,7 @@
    7.13    "ADD_CLAUSES" > "HOL4Base.arithmetic.ADD_CLAUSES"
    7.14    "ADD_ASSOC" > "Finite_Set.AC_add.f.AC_1"
    7.15    "ADD_0" > "Finite_Set.AC_add.f_e.ident"
    7.16 -  "ADD1" > "Presburger.Suc_plus1"
    7.17 +  "ADD1" > "Nat_Numeral.Suc_eq_plus1"
    7.18    "ADD" > "HOL4Compat.ADD"
    7.19  
    7.20  end
     8.1 --- a/src/HOL/Library/Formal_Power_Series.thy	Tue Jun 23 21:07:39 2009 +0200
     8.2 +++ b/src/HOL/Library/Formal_Power_Series.thy	Wed Jun 24 09:41:14 2009 +0200
     8.3 @@ -1615,7 +1615,7 @@
     8.4  	  fix v assume v: "v \<in> {xs \<in> natpermute n (Suc k). n \<in> set xs}"
     8.5  	  let ?ths = "(\<Prod>j\<in>{0..k}. a $ v ! j) = a $ n * (?r$0)^k"
     8.6  	  from v obtain i where i: "i \<in> {0..k}" "v = replicate (k+1) 0 [i:= n]"
     8.7 -	    unfolding Suc_plus1 natpermute_contain_maximal by (auto simp del: replicate.simps)
     8.8 +	    unfolding Suc_eq_plus1 natpermute_contain_maximal by (auto simp del: replicate.simps)
     8.9  	  have "(\<Prod>j\<in>{0..k}. a $ v ! j) = (\<Prod>j\<in>{0..k}. if j = i then a $ n else r (Suc k) (b$0))"
    8.10  	    apply (rule setprod_cong, simp)
    8.11  	    using i a0 by (simp del: replicate.simps)
    8.12 @@ -1651,7 +1651,7 @@
    8.13  	from H have "b$n = a^Suc k $ n" by (simp add: fps_eq_iff)
    8.14  	also have "a ^ Suc k$n = setsum ?g ?Pnkn + setsum ?g ?Pnknn"
    8.15  	  unfolding fps_power_nth_Suc
    8.16 -	  using setsum_Un_disjoint[OF f d, unfolded Suc_plus1[symmetric],
    8.17 +	  using setsum_Un_disjoint[OF f d, unfolded Suc_eq_plus1[symmetric],
    8.18  	    unfolded eq, of ?g] by simp
    8.19  	also have "\<dots> = of_nat (k+1) * a $ n * (?r $ 0)^k + setsum ?f ?Pnknn" unfolding th0 th1 ..
    8.20  	finally have "of_nat (k+1) * a $ n * (?r $ 0)^k = b$n - setsum ?f ?Pnknn" by simp
     9.1 --- a/src/HOL/MetisExamples/BT.thy	Tue Jun 23 21:07:39 2009 +0200
     9.2 +++ b/src/HOL/MetisExamples/BT.thy	Wed Jun 24 09:41:14 2009 +0200
     9.3 @@ -171,7 +171,7 @@
     9.4  ML {*AtpWrapper.problem_name := "BT__n_leaves_bt_map"*}
     9.5  lemma n_leaves_bt_map [simp]: "n_leaves (bt_map f t) = n_leaves t"
     9.6    apply (induct t)
     9.7 -  apply (metis One_nat_def Suc_eq_add_numeral_1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1))
     9.8 +  apply (metis One_nat_def Suc_eq_plus1 bt_map.simps(1) less_add_one less_antisym linorder_neq_iff n_leaves.simps(1))
     9.9    apply (metis bt_map.simps(2) n_leaves.simps(2))
    9.10    done
    9.11  
    10.1 --- a/src/HOL/Nat_Numeral.thy	Tue Jun 23 21:07:39 2009 +0200
    10.2 +++ b/src/HOL/Nat_Numeral.thy	Wed Jun 24 09:41:14 2009 +0200
    10.3 @@ -521,10 +521,10 @@
    10.4  
    10.5  subsubsection{*Arith *}
    10.6  
    10.7 -lemma Suc_eq_add_numeral_1: "Suc n = n + 1"
    10.8 +lemma Suc_eq_plus1: "Suc n = n + 1"
    10.9  by (simp add: numerals)
   10.10  
   10.11 -lemma Suc_eq_add_numeral_1_left: "Suc n = 1 + n"
   10.12 +lemma Suc_eq_plus1_left: "Suc n = 1 + n"
   10.13  by (simp add: numerals)
   10.14  
   10.15  (* These two can be useful when m = number_of... *)
    11.1 --- a/src/HOL/Presburger.thy	Tue Jun 23 21:07:39 2009 +0200
    11.2 +++ b/src/HOL/Presburger.thy	Wed Jun 24 09:41:14 2009 +0200
    11.3 @@ -399,7 +399,6 @@
    11.4  lemma number_of1: "(0::int) <= number_of n \<Longrightarrow> (0::int) <= number_of (Int.Bit0 n) \<and> (0::int) <= number_of (Int.Bit1 n)"
    11.5  by simp
    11.6  lemma number_of2: "(0::int) <= Numeral0" by simp
    11.7 -lemma Suc_plus1: "Suc n = n + 1" by simp
    11.8  
    11.9  text {*
   11.10    \medskip Specific instances of congruence rules, to prevent
    12.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Tue Jun 23 21:07:39 2009 +0200
    12.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Wed Jun 24 09:41:14 2009 +0200
    12.3 @@ -61,7 +61,7 @@
    12.4      (HOL_basic_ss 
    12.5         addsimps @{thms arith_simps} @ natarith @ @{thms rel_simps}
    12.6               @ [if_False, if_True, @{thm add_0}, @{thm add_Suc},
    12.7 -                 @{thm add_number_of_left}, @{thm Suc_eq_add_numeral_1}]
    12.8 +                 @{thm add_number_of_left}, @{thm Suc_eq_plus1}]
    12.9               @ map (fn th => th RS sym) @{thms numerals}));
   12.10  
   12.11  val nat_mul_conv = nat_add_conv;
    13.1 --- a/src/HOL/Tools/Qelim/presburger.ML	Tue Jun 23 21:07:39 2009 +0200
    13.2 +++ b/src/HOL/Tools/Qelim/presburger.ML	Wed Jun 24 09:41:14 2009 +0200
    13.3 @@ -118,7 +118,7 @@
    13.4  val ss2 = HOL_basic_ss
    13.5    addsimps [@{thm "nat_0_le"}, @{thm "int_nat_number_of"},
    13.6              @{thm "all_nat"}, @{thm "ex_nat"}, @{thm "number_of1"}, 
    13.7 -            @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_plus1"}]
    13.8 +            @{thm "number_of2"}, @{thm "int_0"}, @{thm "int_1"}, @{thm "Suc_eq_plus1"}]
    13.9    addcongs [@{thm "conj_le_cong"}, @{thm "imp_le_cong"}]
   13.10  val div_mod_ss = HOL_basic_ss addsimps simp_thms 
   13.11    @ map (symmetric o mk_meta_eq) 
   13.12 @@ -129,7 +129,7 @@
   13.13       @{thm "div_by_0"}, @{thm "DIVISION_BY_ZERO"} RS conjunct1, 
   13.14       @{thm "DIVISION_BY_ZERO"} RS conjunct2, @{thm "zdiv_zero"}, @{thm "zmod_zero"}, 
   13.15       @{thm "div_0"}, @{thm "mod_0"}, @{thm "div_by_1"}, @{thm "mod_by_1"}, @{thm "div_1"}, 
   13.16 -     @{thm "mod_1"}, @{thm "Suc_plus1"}]
   13.17 +     @{thm "mod_1"}, @{thm "Suc_eq_plus1"}]
   13.18    @ @{thms add_ac}
   13.19   addsimprocs [cancel_div_mod_nat_proc, cancel_div_mod_int_proc]
   13.20   val splits_ss = comp_ss addsimps [@{thm "mod_div_equality'"}] addsplits 
    14.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Tue Jun 23 21:07:39 2009 +0200
    14.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Wed Jun 24 09:41:14 2009 +0200
    14.3 @@ -152,7 +152,7 @@
    14.4    fun trans_tac _       = Arith_Data.trans_tac
    14.5  
    14.6    val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @
    14.7 -    [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
    14.8 +    [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
    14.9    val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   14.10    fun norm_tac ss = 
   14.11      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   14.12 @@ -240,7 +240,7 @@
   14.13    val prove_conv        = Arith_Data.prove_conv_nohyps
   14.14    fun trans_tac _       = Arith_Data.trans_tac
   14.15  
   14.16 -  val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1}] @ @{thms add_ac}
   14.17 +  val norm_ss1 = Numeral_Simprocs.num_ss addsimps numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1}] @ @{thms add_ac}
   14.18    val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   14.19    fun norm_tac ss =
   14.20      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
   14.21 @@ -266,7 +266,7 @@
   14.22    fun trans_tac _       = Arith_Data.trans_tac
   14.23  
   14.24    val norm_ss1 = Numeral_Simprocs.num_ss addsimps
   14.25 -    numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_add_numeral_1_left}] @ @{thms add_ac}
   14.26 +    numeral_syms @ add_0s @ mult_1s @ [@{thm Suc_eq_plus1_left}] @ @{thms add_ac}
   14.27    val norm_ss2 = Numeral_Simprocs.num_ss addsimps bin_simps @ @{thms add_ac} @ @{thms mult_ac}
   14.28    fun norm_tac ss =
   14.29      ALLGOALS (simp_tac (Simplifier.inherit_context ss norm_ss1))
    15.1 --- a/src/HOL/Transcendental.thy	Tue Jun 23 21:07:39 2009 +0200
    15.2 +++ b/src/HOL/Transcendental.thy	Wed Jun 24 09:41:14 2009 +0200
    15.3 @@ -2242,7 +2242,7 @@
    15.4  lemma tan_periodic_nat[simp]: fixes n :: nat shows "tan (x + real n * pi) = tan x" 
    15.5  proof (induct n arbitrary: x)
    15.6    case (Suc n)
    15.7 -  have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
    15.8 +  have split_pi_off: "x + real (Suc n) * pi = (x + real n * pi) + pi" unfolding Suc_eq_plus1 real_of_nat_add real_of_one real_add_mult_distrib by auto
    15.9    show ?case unfolding split_pi_off using Suc by auto
   15.10  qed auto
   15.11  
   15.12 @@ -2779,12 +2779,12 @@
   15.13      show ?thesis
   15.14      proof (cases "0 \<le> x")
   15.15        case True from mono[OF this `x \<le> 1`, THEN allI]
   15.16 -      show ?thesis unfolding Suc_plus1[symmetric] by (rule mono_SucI2)
   15.17 +      show ?thesis unfolding Suc_eq_plus1[symmetric] by (rule mono_SucI2)
   15.18      next
   15.19        case False hence "0 \<le> -x" and "-x \<le> 1" using `-1 \<le> x` by auto
   15.20        from mono[OF this]
   15.21        have "\<And>n. 1 / real (Suc (Suc n * 2)) * x ^ Suc (Suc n * 2) \<ge> 1 / real (Suc (n * 2)) * x ^ Suc (n * 2)" using `0 \<le> -x` by auto
   15.22 -      thus ?thesis unfolding Suc_plus1[symmetric] by (rule mono_SucI1[OF allI])
   15.23 +      thus ?thesis unfolding Suc_eq_plus1[symmetric] by (rule mono_SucI1[OF allI])
   15.24      qed
   15.25    qed
   15.26  qed
   15.27 @@ -2800,13 +2800,13 @@
   15.28      case True hence "norm x < 1" by auto
   15.29      from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat LIMSEQ_power_zero[OF `norm x < 1`, THEN LIMSEQ_Suc]]
   15.30      have "(\<lambda>n. 1 / real (n + 1) * x ^ (n + 1)) ----> 0"
   15.31 -      unfolding inverse_eq_divide Suc_plus1 by simp
   15.32 +      unfolding inverse_eq_divide Suc_eq_plus1 by simp
   15.33      then show ?thesis using pos2 by (rule LIMSEQ_linear)
   15.34    next
   15.35      case False hence "x = -1 \<or> x = 1" using `\<bar>x\<bar> \<le> 1` by auto
   15.36      hence n_eq: "\<And> n. x ^ (n * 2 + 1) = x" unfolding One_nat_def by auto
   15.37      from LIMSEQ_mult[OF LIMSEQ_inverse_real_of_nat[THEN LIMSEQ_linear, OF pos2, unfolded inverse_eq_divide] LIMSEQ_const[of x]]
   15.38 -    show ?thesis unfolding n_eq Suc_plus1 by auto
   15.39 +    show ?thesis unfolding n_eq Suc_eq_plus1 by auto
   15.40    qed
   15.41  qed
   15.42  
   15.43 @@ -2921,7 +2921,7 @@
   15.44      qed
   15.45      
   15.46      have suminf_arctan_zero: "suminf (?c 0) - arctan 0 = 0"
   15.47 -      unfolding Suc_plus1[symmetric] power_Suc2 mult_zero_right arctan_zero_zero suminf_zero by auto
   15.48 +      unfolding Suc_eq_plus1[symmetric] power_Suc2 mult_zero_right arctan_zero_zero suminf_zero by auto
   15.49      
   15.50      have "suminf (?c x) - arctan x = 0"
   15.51      proof (cases "x = 0")
    16.1 --- a/src/HOL/Word/BinBoolList.thy	Tue Jun 23 21:07:39 2009 +0200
    16.2 +++ b/src/HOL/Word/BinBoolList.thy	Wed Jun 24 09:41:14 2009 +0200
    16.3 @@ -658,7 +658,7 @@
    16.4    apply (unfold bl_to_bin_def)
    16.5    apply (induct n)
    16.6     apply simp
    16.7 -  apply (simp only: Suc_eq_add_numeral_1 replicate_add
    16.8 +  apply (simp only: Suc_eq_plus1 replicate_add
    16.9                      append_Cons [symmetric] bl_to_bin_aux_append)
   16.10    apply simp
   16.11    done