src/HOL/Number_Theory/Fib.thy

--- a/src/HOL/Number_Theory/Fib.thy	Sun Aug 18 18:49:45 2013 +0200
+++ b/src/HOL/Number_Theory/Fib.thy	Sun Aug 18 19:59:19 2013 +0200
@@ -169,24 +169,24 @@
 *}
 
 lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
-    (fib (int n + 1))^2 = (-1)^(n + 1)"
+    (fib (int n + 1))\<^sup>2 = (-1)^(n + 1)"
   apply (induct n)
   apply (auto simp add: field_simps power2_eq_square fib_reduce_int power_add)
   done
 
 lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
-    (fib (n + 1))^2 = (-1)^(nat n + 1)"
+    (fib (n + 1))\<^sup>2 = (-1)^(nat n + 1)"
   by (insert fib_Cassini_aux_int [of "nat n"], auto)
 
 (*
 lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
-    (fib (n + 1))^2 + (-1)^(nat n + 1)"
+    (fib (n + 1))\<^sup>2 + (-1)^(nat n + 1)"
   by (frule fib_Cassini_int, simp)
 *)
 
 lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
-  (if even n then tsub ((fib (n + 1))^2) 1
-   else (fib (n + 1))^2 + 1)"
+  (if even n then tsub ((fib (n + 1))\<^sup>2) 1
+   else (fib (n + 1))\<^sup>2 + 1)"
   apply (frule fib_Cassini_int, auto simp add: pos_int_even_equiv_nat_even)
   apply (subst tsub_eq)
   apply (insert fib_gr_0_int [of "n + 1"], force)
@@ -194,8 +194,8 @@
   done
 
 lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n =
-    (if even n then (fib (n + 1))^2 - 1
-     else (fib (n + 1))^2 + 1)"
+    (if even n then (fib (n + 1))\<^sup>2 - 1
+     else (fib (n + 1))\<^sup>2 + 1)"
   by (rule fib_Cassini'_int [transferred, of n], auto)