diff -r 0ce594837524 -r fa53d267dab3 src/HOL/Isar_Examples/Fibonacci.thy
--- a/src/HOL/Isar_Examples/Fibonacci.thy	Thu Jul 01 14:32:57 2010 +0200
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Thu Jul 01 18:31:46 2010 +0200
@@ -15,22 +15,20 @@
 header {* Fib and Gcd commute *}
 
 theory Fibonacci
-imports Primes
+imports "../Old_Number_Theory/Primes"
 begin
 
-text_raw {*
- \footnote{Isar version by Gertrud Bauer.  Original tactic script by
- Larry Paulson.  A few proofs of laws taken from
- \cite{Concrete-Math}.}
-*}
+text_raw {* \footnote{Isar version by Gertrud Bauer.  Original tactic
+  script by Larry Paulson.  A few proofs of laws taken from
+  \cite{Concrete-Math}.} *}
 
 
 subsection {* Fibonacci numbers *}
 
 fun fib :: "nat \<Rightarrow> nat" where
   "fib 0 = 0"
-  | "fib (Suc 0) = 1"
-  | "fib (Suc (Suc x)) = fib x + fib (Suc x)"
+| "fib (Suc 0) = 1"
+| "fib (Suc (Suc x)) = fib x + fib (Suc x)"
 
 lemma [simp]: "0 < fib (Suc n)"
   by (induct n rule: fib.induct) simp_all
@@ -102,7 +100,7 @@
   then have "gcd (fib m) (fib (n + m)) = gcd (fib (n + k + 1)) (fib (k + 1))"
     by (simp add: gcd_commute)
   also have "fib (n + k + 1)
-    = fib (k + 1) * fib (n + 1) + fib k * fib n"
+      = fib (k + 1) * fib (n + 1) + fib k * fib n"
     by (rule fib_add)
   also have "gcd ... (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
     by (simp add: gcd_mult_add)
@@ -139,18 +137,17 @@
       case False then have "m <= n" by simp
       from `0 < m` and False have "n - m < n" by simp
       with hyp have "gcd (fib m) (fib ((n - m) mod m))
-        = gcd (fib m) (fib (n - m))" by simp
+          = gcd (fib m) (fib (n - m))" by simp
       also have "... = gcd (fib m) (fib n)"
         using `m <= n` by (rule gcd_fib_diff)
       finally have "gcd (fib m) (fib ((n - m) mod m)) =
-        gcd (fib m) (fib n)" .
+          gcd (fib m) (fib n)" .
       with False show ?thesis by simp
     qed
     finally show ?thesis .
   qed
 qed
 
-
 theorem fib_gcd: "fib (gcd m n) = gcd (fib m) (fib n)" (is "?P m n")
 proof (induct m n rule: gcd_induct)
   fix m show "fib (gcd m 0) = gcd (fib m) (fib 0)" by simp