proper naming of fib equations;
authorwenzelm
Sat Apr 01 20:22:46 2000 +0200 (2000-04-01)
changeset 86583cf533397c5a
parent 8657 b9475dad85ed
child 8659 5fdbe2dd54f9
proper naming of fib equations;
src/HOL/ex/Fib.ML
src/HOL/ex/Fib.thy
     1.1 --- a/src/HOL/ex/Fib.ML	Sat Apr 01 20:21:39 2000 +0200
     1.2 +++ b/src/HOL/ex/Fib.ML	Sat Apr 01 20:22:46 2000 +0200
     1.3 @@ -17,9 +17,9 @@
     1.4      selectively at first.
     1.5  **)
     1.6  
     1.7 -val [fib_Suc_Suc] = thms"fib.2";
     1.8 -Delsimps [fib_Suc_Suc];
     1.9 +Delsimps fib.Suc_Suc;
    1.10  
    1.11 +val [fib_Suc_Suc] = fib.Suc_Suc;
    1.12  val fib_Suc3 = read_instantiate [("x", "(Suc ?n)")] fib_Suc_Suc;
    1.13  
    1.14  (*Concrete Mathematics, page 280*)
     2.1 --- a/src/HOL/ex/Fib.thy	Sat Apr 01 20:21:39 2000 +0200
     2.2 +++ b/src/HOL/ex/Fib.thy	Sat Apr 01 20:22:46 2000 +0200
     2.3 @@ -10,8 +10,8 @@
     2.4  
     2.5  consts fib  :: "nat => nat"
     2.6  recdef fib "less_than"
     2.7 -    "fib 0 = 0"
     2.8 -    "fib 1 = 1"
     2.9 -    "fib (Suc(Suc x)) = (fib x + fib (Suc x))"
    2.10 +  zero    "fib 0 = 0"
    2.11 +  one     "fib 1 = 1"
    2.12 +  Suc_Suc "fib (Suc (Suc x)) = fib x + fib (Suc x)"
    2.13  
    2.14  end