# HG changeset patch
# User paulson
# Date 997195012 -7200
# Node ID 02cd5d5bc4974207dc4476b0e0a7f5e6f396117f
# Parent  1064effe37f6bcea84da4d411cf905e0c478024b
Tweaks for 1 -> 1'

diff -r 1064effe37f6 -r 02cd5d5bc497 src/HOL/GroupTheory/Exponent.ML
--- a/src/HOL/GroupTheory/Exponent.ML	Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/GroupTheory/Exponent.ML	Tue Aug 07 16:36:52 2001 +0200
@@ -8,11 +8,11 @@
 
 val prime_def = thm "prime_def";
 
-Goalw [prime_def] "p\\<in>prime ==> 1 < p";
-by (Blast_tac 1); 
+Goalw [prime_def] "p\\<in>prime ==> 1' < p";
+by (force_tac (claset(), simpset() addsimps []) 1); 
 qed "prime_imp_one_less";
 
-Goal "(p\\<in>prime) = (1<p & (\\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))";
+Goal "(p\\<in>prime) = (1'<p & (\\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))";
 by (auto_tac (claset(), simpset() addsimps [prime_imp_one_less]));  
 by (blast_tac (claset() addSDs [thm "prime_dvd_mult"]) 1);
 by (auto_tac (claset(), simpset() addsimps [prime_def]));  
@@ -23,6 +23,7 @@
 by (dres_inst_tac [("x","k")] spec 1);
 by (asm_full_simp_tac
     (simpset() addsimps [dvd_mult_cancel1, dvd_mult_cancel2]) 1);  
+by Auto_tac; 
 qed "prime_iff";
 
 Goal "p\\<in>prime ==> 0 < p^a";
@@ -106,9 +107,7 @@
 by (res_inst_tac [("P","%x. x <= b * c")] subst 1);
 by (rtac mult_1_right 1);
 by (rtac mult_le_mono 1);
-by (assume_tac 1);
-by (stac Suc_le_eq 1);
-by (assume_tac 1);
+by Auto_tac; 
 qed "le_extend_mult";
 
 
@@ -194,15 +193,15 @@
 qed_spec_mp "prime_power_dvd_cases";
 
 (*needed in this form in Sylow.ML*)
-Goal "[| p\\<in>prime; ~(p ^ (r+1) dvd n); p ^ (a+r) dvd n * k |] \
+Goal "[| p \\<in> prime; ~ (p ^ (Suc r) dvd n);  p^(a+r) dvd n*k |] \
 \     ==> p ^ a dvd k";
-by (dres_inst_tac [("a","r+1"), ("b","a")] prime_power_dvd_cases 1);
+by (dres_inst_tac [("a","Suc r"), ("b","a")] prime_power_dvd_cases 1);
 by (assume_tac 1);  
 by Auto_tac;  
 qed "div_combine";
 
 (*Lemma for power_dvd_bound*)
-Goal "1 < p ==> Suc n <= p^n";
+Goal "1' < p ==> Suc n <= p^n";
 by (induct_tac "n" 1);
 by (Asm_simp_tac 1); 
 by (Asm_full_simp_tac 1); 
@@ -219,7 +218,7 @@
 qed "Suc_le_power";
 
 (*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
-Goal "[|p^n dvd a;  1 < p;  0 < a|] ==> n < a";
+Goal "[|p^n dvd a;  1' < p;  0 < a|] ==> n < a";
 by (dtac dvd_imp_le 1); 
 by (dres_inst_tac [("n","n")] Suc_le_power 2); 
 by Auto_tac;  
@@ -254,7 +253,7 @@
 by (asm_simp_tac (simpset() addsimps [exponent_def]) 1);
 by (rtac Greatest_equality 1); 
 by (Asm_full_simp_tac 1);
-by (blast_tac (claset() addIs [prime_imp_one_less, power_dvd_imp_le]) 1); 
+by (asm_simp_tac (simpset() addsimps [prime_imp_one_less, power_dvd_imp_le]) 1); 
 qed "exponent_power_eq";
 Addsimps [exponent_power_eq];
 
@@ -268,7 +267,7 @@
 Addsimps [exponent_eq_0];
 
 
-(* exponent_mult_add, easy inclusion.  Could weaken p\\<in>prime to 1<p *)
+(* exponent_mult_add, easy inclusion.  Could weaken p\\<in>prime to 1'<p *)
 Goal "[| 0 < a; 0 < b |]  \
 \     ==> (exponent p a) + (exponent p b) <= exponent p (a * b)";
 by (case_tac "p \\<in> prime" 1);
@@ -313,7 +312,7 @@
 by (auto_tac (claset() addDs [dvd_mult_left], simpset()));  
 qed "not_divides_exponent_0";
 
-Goal "exponent p 1 = 0";
+Goal "exponent p 1' = 0";
 by (case_tac "p \\<in> prime" 1);
 by (auto_tac (claset(), 
               simpset() addsimps [prime_iff, not_divides_exponent_0]));
@@ -358,7 +357,7 @@
 
 
 Goal "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a";
-by (res_inst_tac [("m","1")] p_fac_forw_lemma 1);
+by (res_inst_tac [("m","1'")] p_fac_forw_lemma 1);
 by Auto_tac;
 qed "r_le_a_forw";
 
@@ -423,7 +422,7 @@
 qed "p_not_div_choose";
 
 
-Goal "0 < m ==> exponent p ((p^a * m - 1) choose (p^a - 1)) = 0";
+Goal "0 < m ==> exponent p ((p^a * m - 1') choose (p^a - 1')) = 0";
 by (case_tac "p \\<in> prime" 1);
 by (Asm_simp_tac 2);
 by (forw_inst_tac [("a","a")] zero_less_prime_power 1);
diff -r 1064effe37f6 -r 02cd5d5bc497 src/HOL/GroupTheory/Sylow.ML
--- a/src/HOL/GroupTheory/Sylow.ML	Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/GroupTheory/Sylow.ML	Tue Aug 07 16:36:52 2001 +0200
@@ -127,7 +127,7 @@
                                   le_extend_mult, zero_less_m]) 1); 
 qed "zero_less_card_calM";
 
-Goal "~(p ^ (exponent p m+ 1) dvd card(calM))";
+Goal "~ (p ^ Suc(exponent p m) dvd card(calM))";
 by (subgoal_tac "exponent p m = exponent p (card calM)" 1);
  by (asm_full_simp_tac (simpset() addsimps [card_calM, 
                            zero_less_m RS const_p_fac]) 2);
@@ -140,7 +140,7 @@
 by Auto_tac; 
 qed "finite_calM";
 
-Goal "\\<exists>M \\<in> calM // RelM. ~(p ^ ((exponent p m)+ 1) dvd card(M))";
+Goal "\\<exists>M \\<in> calM // RelM. ~ (p ^ Suc(exponent p m) dvd card(M))";
 by (rtac (max_p_div_calM RS contrapos_np) 1); 
 by (asm_full_simp_tac (simpset() addsimps [finite_calM, 
                           RelM_equiv RSN(2, equiv_imp_dvd_card)]) 1); 
diff -r 1064effe37f6 -r 02cd5d5bc497 src/HOL/GroupTheory/Sylow.thy
--- a/src/HOL/GroupTheory/Sylow.thy	Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/GroupTheory/Sylow.thy	Tue Aug 07 16:36:52 2001 +0200
@@ -36,7 +36,7 @@
     M1 :: "'a set"
   assumes
     M_in_quot "M \\<in> calM // RelM"
-    not_dvd_M "~(p ^ (exponent p m + 1) dvd card(M))"
+    not_dvd_M "~(p ^ Suc(exponent p m) dvd card(M))"
     M1_in_M   "M1 \\<in> M"
   defines
    H_def "H == {g. g\\<in>carrier G & M1 #> g = M1}"
diff -r 1064effe37f6 -r 02cd5d5bc497 src/HOL/Hyperreal/HyperNat.ML
--- a/src/HOL/Hyperreal/HyperNat.ML	Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/Hyperreal/HyperNat.ML	Tue Aug 07 16:36:52 2001 +0200
@@ -682,7 +682,7 @@
 Goalw [hypnat_one_def,hypnat_zero_def,hypnat_less_def] 
       "(0::hypnat) < 1hn";
 by (res_inst_tac [("x","%n. 0")] exI 1);
-by (res_inst_tac [("x","%n. 1")] exI 1);
+by (res_inst_tac [("x","%n. 1'")] exI 1);
 by Auto_tac;
 qed "hypnat_zero_less_one";
 
@@ -806,11 +806,11 @@
 by Auto_tac;
 qed "hypnat_of_nat_le_iff";
 
-Goalw [hypnat_of_nat_def,hypnat_one_def] "hypnat_of_nat  1 = 1hn";
+Goalw [hypnat_of_nat_def,hypnat_one_def] "hypnat_of_nat 1' = 1hn";
 by (Simp_tac 1);
 qed "hypnat_of_nat_one";
 
-Goalw [hypnat_of_nat_def,hypnat_zero_def] "hypnat_of_nat  0 = 0";
+Goalw [hypnat_of_nat_def,hypnat_zero_def] "hypnat_of_nat 0 = 0";
 by (Simp_tac 1);
 qed "hypnat_of_nat_zero";
 
@@ -903,7 +903,7 @@
 qed "SHNat_hypnat_of_nat";
 Addsimps [SHNat_hypnat_of_nat];
 
-Goal "hypnat_of_nat 1 : Nats";
+Goal "hypnat_of_nat 1' : Nats";
 by (Simp_tac 1);
 qed "SHNat_hypnat_of_nat_one";
 
diff -r 1064effe37f6 -r 02cd5d5bc497 src/HOL/Hyperreal/HyperPow.ML
--- a/src/HOL/Hyperreal/HyperPow.ML	Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/Hyperreal/HyperPow.ML	Tue Aug 07 16:36:52 2001 +0200
@@ -33,7 +33,7 @@
 by (auto_tac (claset(), simpset() addsimps hypreal_mult_ac));
 qed "hrealpow_add";
 
-Goal "(r::hypreal) ^ 1 = r";
+Goal "(r::hypreal) ^ 1' = r";
 by (Simp_tac 1);
 qed "hrealpow_one";
 Addsimps [hrealpow_one];
diff -r 1064effe37f6 -r 02cd5d5bc497 src/HOL/Hyperreal/Lim.ML
--- a/src/HOL/Hyperreal/Lim.ML	Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/Hyperreal/Lim.ML	Tue Aug 07 16:36:52 2001 +0200
@@ -1294,7 +1294,7 @@
 qed "NSDERIV_cmult_Id";
 Addsimps [NSDERIV_cmult_Id];
 
-Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - 1))";
+Goal "DERIV (%x. x ^ n) x :> real n * (x ^ (n - 1'))";
 by (induct_tac "n" 1);
 by (dtac (DERIV_Id RS DERIV_mult) 2);
 by (auto_tac (claset(), 
@@ -1306,7 +1306,7 @@
 qed "DERIV_pow";
 
 (* NS version *)
-Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - 1))";
+Goal "NSDERIV (%x. x ^ n) x :> real n * (x ^ (n - 1'))";
 by (simp_tac (simpset() addsimps [NSDERIV_DERIV_iff, DERIV_pow]) 1);
 qed "NSDERIV_pow";
 
diff -r 1064effe37f6 -r 02cd5d5bc497 src/HOL/Hyperreal/Series.ML
--- a/src/HOL/Hyperreal/Series.ML	Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/Hyperreal/Series.ML	Tue Aug 07 16:36:52 2001 +0200
@@ -191,28 +191,17 @@
 by (Auto_tac);
 qed "sumr_zero";
 
-Goal "Suc N <= n --> N <= n - 1";
-by (induct_tac "n" 1);
-by (Auto_tac);
-qed_spec_mp "Suc_le_imp_diff_ge";
-
 Goal "ALL n. N <= n --> f (Suc n) = #0 \
 \     ==> ALL m n. Suc N <= m --> sumr m n f = #0";   
 by (rtac sumr_zero 1 THEN Step_tac 1);
-by (subgoal_tac "0 < n" 1);
-by (dtac Suc_le_imp_diff_ge 1);
-by (Auto_tac);
+by (case_tac "n" 1);
+by Auto_tac; 
 qed "Suc_le_imp_diff_ge2";
 
-(* proved elsewhere? *)
-Goal "(0 < n) = (EX m. n = Suc m)";
+Goal "sumr 1' n (%n. f(n) * #0 ^ n) = #0";
 by (induct_tac "n" 1);
-by (Auto_tac);
-qed "gt_zero_eq_Ex";
-
-Goal "sumr 1 n (%n. f(n) * #0 ^ n) = #0";
-by (induct_tac "n" 1);
-by (auto_tac (claset(),simpset() addsimps [gt_zero_eq_Ex]));
+by (case_tac "n" 2);
+by Auto_tac; 
 qed "sumr_one_lb_realpow_zero";
 Addsimps [sumr_one_lb_realpow_zero];
 
@@ -220,7 +209,7 @@
 by (simp_tac (simpset() addsimps [sumr_add RS sym,sumr_minus]) 1);
 qed "sumr_diff";
 
-Goal "(ALL p. (m <= p & p < m + n --> (f p = g p))) --> sumr m n f = sumr m n g";
+Goal "(ALL p. m <= p & p < m+n --> (f p = g p)) --> sumr m n f = sumr m n g";
 by (induct_tac "n" 1);
 by (Auto_tac);
 qed_spec_mp "sumr_subst";
@@ -564,7 +553,8 @@
 by (asm_full_simp_tac (simpset() addsimps [summable_Cauchy]) 1);
 by (Step_tac 1 THEN subgoal_tac "ALL n. N <= n --> f (Suc n) = #0" 1);
 by (blast_tac (claset() addIs [rabs_ratiotest_lemma]) 2);
-by (res_inst_tac [("x","Suc N")] exI 1 THEN Step_tac 1);
+by (res_inst_tac [("x","Suc N")] exI 1);
+by (Clarify_tac 1); 
 by (dtac Suc_le_imp_diff_ge2 1 THEN Auto_tac);
 qed "ratio_test_lemma2";
 
diff -r 1064effe37f6 -r 02cd5d5bc497 src/HOL/Integ/NatBin.thy
--- a/src/HOL/Integ/NatBin.thy	Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/Integ/NatBin.thy	Tue Aug 07 16:36:52 2001 +0200
@@ -18,10 +18,6 @@
     "number_of v == nat (number_of v)"
      (*::bin=>nat        ::bin=>int*)
 
-axioms
-neg_number_of_bin_pred_iff_0:
-  "neg (number_of (bin_pred v)) = (number_of v = (0::nat))"
-
 use "nat_bin.ML"	setup nat_bin_arith_setup
 
 end
diff -r 1064effe37f6 -r 02cd5d5bc497 src/HOL/Integ/NatSimprocs.ML
--- a/src/HOL/Integ/NatSimprocs.ML	Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/Integ/NatSimprocs.ML	Tue Aug 07 16:36:52 2001 +0200
@@ -14,15 +14,12 @@
 
 (*Now just instantiating n to (number_of v) does the right simplification,
   but with some redundant inequality tests.*)
-(*
 Goal "neg (number_of (bin_pred v)) = (number_of v = (0::nat))";
-by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1)" 1);
-by (Asm_simp_tac 1);
+by (subgoal_tac "neg (number_of (bin_pred v)) = (number_of v < 1')" 1);
+by (asm_simp_tac (HOL_ss addsimps [less_Suc_eq_le, le_0_eq]) 1); 
 by (stac less_number_of_Suc 1);
 by (Simp_tac 1);
 qed "neg_number_of_bin_pred_iff_0";
-*)
-val neg_number_of_bin_pred_iff_0 = thm "neg_number_of_bin_pred_iff_0";
 
 Goal "neg (number_of (bin_minus v)) ==> \
 \     Suc m - (number_of v) = m - (number_of (bin_pred v))";
diff -r 1064effe37f6 -r 02cd5d5bc497 src/HOL/NatArith.ML
--- a/src/HOL/NatArith.ML	Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/NatArith.ML	Tue Aug 07 16:36:52 2001 +0200
@@ -96,17 +96,17 @@
 
 (** Lemmas for ex/Factorization **)
 
-Goal "!!m::nat. [| 1<n; 1<m |] ==> 1<m*n";
+Goal "!!m::nat. [| 1' < n; 1' < m |] ==> 1' < m*n";
 by (case_tac "m" 1);
 by Auto_tac;
 qed "one_less_mult"; 
 
-Goal "!!m::nat. [| 1<n; 1<m |] ==> n<m*n";
+Goal "!!m::nat. [| 1' < n; 1' < m |] ==> n<m*n";
 by (case_tac "m" 1);
 by Auto_tac;
 qed "n_less_m_mult_n"; 
 
-Goal "!!m::nat. [| 1<n; 1<m |] ==> n<n*m";
+Goal "!!m::nat. [| 1' < n; 1' < m |] ==> n<n*m";
 by (case_tac "m" 1);
 by Auto_tac;
 qed "n_less_n_mult_m"; 
diff -r 1064effe37f6 -r 02cd5d5bc497 src/HOL/NumberTheory/Chinese.thy
--- a/src/HOL/NumberTheory/Chinese.thy	Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/NumberTheory/Chinese.thy	Tue Aug 07 16:36:52 2001 +0200
@@ -56,9 +56,9 @@
 
   mhf_def:
     "mhf mf n i ==
-      if i = 0 then funprod mf 1 (n - 1)
-      else if i = n then funprod mf 0 (n - 1)
-      else funprod mf 0 (i - 1) * funprod mf (i + 1) (n - 1 - i)"
+      if i = 0 then funprod mf 1' (n - 1')
+      else if i = n then funprod mf 0 (n - 1')
+      else funprod mf 0 (i - 1') * funprod mf (Suc i) (n - 1' - i)"
 
   xilin_sol_def:
     "xilin_sol i n kf bf mf ==
diff -r 1064effe37f6 -r 02cd5d5bc497 src/HOL/NumberTheory/Factorization.thy
--- a/src/HOL/NumberTheory/Factorization.thy	Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/NumberTheory/Factorization.thy	Tue Aug 07 16:36:52 2001 +0200
@@ -26,7 +26,7 @@
   "nondec (x # xs) = (case xs of [] => True | y # ys => x \<le> y \<and> nondec xs)"
 
 primrec
-  "prod [] = 1"
+  "prod [] = 1'"
   "prod (x # xs) = x * prod xs"
 
 primrec
@@ -40,12 +40,12 @@
 
 subsection {* Arithmetic *}
 
-lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> 1 ==> 1 < m"
+lemma one_less_m: "(m::nat) \<noteq> m * k ==> m \<noteq> 1' ==> 1' < m"
   apply (case_tac m)
    apply auto
   done
 
-lemma one_less_k: "(m::nat) \<noteq> m * k ==> 1 < m * k ==> 1 < k"
+lemma one_less_k: "(m::nat) \<noteq> m * k ==> 1' < m * k ==> 1' < k"
   apply (case_tac k)
    apply auto
   done
@@ -54,13 +54,13 @@
   apply auto
   done
 
-lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = 1"
+lemma mn_eq_m_one: "(0::nat) < m ==> m * n = m ==> n = 1'"
   apply (case_tac n)
    apply auto
   done
 
 lemma prod_mn_less_k:
-    "(0::nat) < n ==> 0 < k ==> 1 < m ==> m * n = k ==> n < k"
+    "(0::nat) < n ==> 0 < k ==> 1' < m ==> m * n = k ==> n < k"
   apply (induct m)
    apply auto
   done
@@ -88,7 +88,7 @@
   apply auto
   done
 
-lemma prime_nd_one: "p \<in> prime ==> \<not> p dvd 1"
+lemma prime_nd_one: "p \<in> prime ==> \<not> p dvd 1'"
   apply (unfold prime_def dvd_def)
   apply auto
   done
@@ -115,13 +115,13 @@
   apply auto
   done
 
-lemma primel_one_empty: "primel xs ==> prod xs = 1 ==> xs = []"
+lemma primel_one_empty: "primel xs ==> prod xs = 1' ==> xs = []"
   apply (unfold primel_def prime_def)
   apply (case_tac xs)
    apply simp_all
   done
 
-lemma prime_g_one: "p \<in> prime ==> 1 < p"
+lemma prime_g_one: "p \<in> prime ==> 1' < p"
   apply (unfold prime_def)
   apply auto
   done
@@ -132,7 +132,7 @@
   done
 
 lemma primel_nempty_g_one [rule_format]:
-    "primel xs --> xs \<noteq> [] --> 1 < prod xs"
+    "primel xs --> xs \<noteq> [] --> 1' < prod xs"
   apply (unfold primel_def prime_def)
   apply (induct xs)
    apply (auto elim: one_less_mult)
@@ -223,8 +223,8 @@
   done
 
 lemma not_prime_ex_mk:
-  "1 < n \<and> n \<notin> prime ==>
-    \<exists>m k. 1 < m \<and> 1 < k \<and> m < n \<and> k < n \<and> n = m * k"
+  "1' < n \<and> n \<notin> prime ==>
+    \<exists>m k. 1' < m \<and> 1' < k \<and> m < n \<and> k < n \<and> n = m * k"
   apply (unfold prime_def dvd_def)
   apply (auto intro: n_less_m_mult_n n_less_n_mult_m one_less_m one_less_k)
   done
@@ -237,7 +237,7 @@
   apply (simp add: primel_append)
   done
 
-lemma factor_exists [rule_format]: "1 < n --> (\<exists>l. primel l \<and> prod l = n)"
+lemma factor_exists [rule_format]: "1' < n --> (\<exists>l. primel l \<and> prod l = n)"
   apply (induct n rule: nat_less_induct)
   apply (rule impI)
   apply (case_tac "n \<in> prime")
@@ -247,7 +247,7 @@
    apply (auto intro!: split_primel)
   done
 
-lemma nondec_factor_exists: "1 < n ==> \<exists>l. primel l \<and> nondec l \<and> prod l = n"
+lemma nondec_factor_exists: "1' < n ==> \<exists>l. primel l \<and> nondec l \<and> prod l = n"
   apply (erule factor_exists [THEN exE])
   apply (blast intro!: ex_nondec_lemma)
   done
@@ -349,7 +349,7 @@
   done
 
 lemma unique_prime_factorization [rule_format]:
-    "\<forall>n. 1 < n --> (\<exists>!l. primel l \<and> nondec l \<and> prod l = n)"
+    "\<forall>n. 1' < n --> (\<exists>!l. primel l \<and> nondec l \<and> prod l = n)"
   apply safe
    apply (erule nondec_factor_exists)
   apply (rule perm_nondec_unique)
diff -r 1064effe37f6 -r 02cd5d5bc497 src/HOL/NumberTheory/Fib.thy
--- a/src/HOL/NumberTheory/Fib.thy	Mon Aug 06 16:43:40 2001 +0200
+++ b/src/HOL/NumberTheory/Fib.thy	Tue Aug 07 16:36:52 2001 +0200
@@ -18,8 +18,8 @@
 
 consts fib :: "nat => nat"
 recdef fib  less_than
-  zero: "fib 0 = 0"
-  one:  "fib 1 = 1"
+  zero: "fib 0  = 0"
+  one:  "fib 1' = 1'"
   Suc_Suc: "fib (Suc (Suc x)) = fib x + fib (Suc x)"
 
 text {*
@@ -81,7 +81,7 @@
 
 text {* \medskip Towards Law 6.111 of Concrete Mathematics *}
 
-lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = 1"
+lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = 1'"
   apply (induct n rule: fib.induct)
     prefer 3
     apply (simp add: gcd_commute fib_Suc3)