src/HOL/ex/Fib.ML

--- a/src/HOL/ex/Fib.ML	Mon Mar 09 16:16:21 1998 +0100
+++ b/src/HOL/ex/Fib.ML	Mon Mar 09 16:17:28 1998 +0100
@@ -49,7 +49,7 @@
 
 (*Concrete Mathematics, page 278: Cassini's identity*)
 goal thy "fib (Suc (Suc n)) * fib n = \
-\              (if n mod 2 = 0 then pred(fib(Suc n) * fib(Suc n)) \
+\              (if n mod 2 = 0 then (fib(Suc n) * fib(Suc n)) - 1 \
 \                              else Suc (fib(Suc n) * fib(Suc n)))";
 by (res_inst_tac [("u","n")] fib.induct 1);
 by (res_inst_tac [("P", "%z. ?ff(x) * z = ?kk(x)")] (fib_Suc_Suc RS ssubst) 3);