src/HOL/NumberTheory/Fib.thy
changeset 11468 02cd5d5bc497
parent 11377 0f16ad464c62
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/NumberTheory/Fib.thy	Mon Aug 06 16:43:40 2001 +0200
     1.2 +++ b/src/HOL/NumberTheory/Fib.thy	Tue Aug 07 16:36:52 2001 +0200
     1.3 @@ -18,8 +18,8 @@
     1.4  
     1.5  consts fib :: "nat => nat"
     1.6  recdef fib  less_than
     1.7 -  zero: "fib 0 = 0"
     1.8 -  one:  "fib 1 = 1"
     1.9 +  zero: "fib 0  = 0"
    1.10 +  one:  "fib 1' = 1'"
    1.11    Suc_Suc: "fib (Suc (Suc x)) = fib x + fib (Suc x)"
    1.12  
    1.13  text {*
    1.14 @@ -81,7 +81,7 @@
    1.15  
    1.16  text {* \medskip Towards Law 6.111 of Concrete Mathematics *}
    1.17  
    1.18 -lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = 1"
    1.19 +lemma gcd_fib_Suc_eq_1: "gcd (fib n, fib (Suc n)) = 1'"
    1.20    apply (induct n rule: fib.induct)
    1.21      prefer 3
    1.22      apply (simp add: gcd_commute fib_Suc3)