1.1 --- a/src/HOL/Number_Theory/Fib.thy	Sun Aug 18 18:49:45 2013 +0200
     1.2 +++ b/src/HOL/Number_Theory/Fib.thy	Sun Aug 18 19:59:19 2013 +0200
     1.3 @@ -169,24 +169,24 @@
     1.4  *}
     1.5  
     1.6  lemma fib_Cassini_aux_int: "fib (int n + 2) * fib (int n) -
     1.7 -    (fib (int n + 1))^2 = (-1)^(n + 1)"
     1.8 +    (fib (int n + 1))\<^sup>2 = (-1)^(n + 1)"
     1.9    apply (induct n)
    1.10    apply (auto simp add: field_simps power2_eq_square fib_reduce_int power_add)
    1.11    done
    1.12  
    1.13  lemma fib_Cassini_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n -
    1.14 -    (fib (n + 1))^2 = (-1)^(nat n + 1)"
    1.15 +    (fib (n + 1))\<^sup>2 = (-1)^(nat n + 1)"
    1.16    by (insert fib_Cassini_aux_int [of "nat n"], auto)
    1.17  
    1.18  (*
    1.19  lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib (n + 2) * fib n =
    1.20 -    (fib (n + 1))^2 + (-1)^(nat n + 1)"
    1.21 +    (fib (n + 1))\<^sup>2 + (-1)^(nat n + 1)"
    1.22    by (frule fib_Cassini_int, simp)
    1.23  *)
    1.24  
    1.25  lemma fib_Cassini'_int: "n >= 0 \<Longrightarrow> fib ((n::int) + 2) * fib n =
    1.26 -  (if even n then tsub ((fib (n + 1))^2) 1
    1.27 -   else (fib (n + 1))^2 + 1)"
    1.28 +  (if even n then tsub ((fib (n + 1))\<^sup>2) 1
    1.29 +   else (fib (n + 1))\<^sup>2 + 1)"
    1.30    apply (frule fib_Cassini_int, auto simp add: pos_int_even_equiv_nat_even)
    1.31    apply (subst tsub_eq)
    1.32    apply (insert fib_gr_0_int [of "n + 1"], force)
    1.33 @@ -194,8 +194,8 @@
    1.34    done
    1.35  
    1.36  lemma fib_Cassini_nat: "fib ((n::nat) + 2) * fib n =
    1.37 -    (if even n then (fib (n + 1))^2 - 1
    1.38 -     else (fib (n + 1))^2 + 1)"
    1.39 +    (if even n then (fib (n + 1))\<^sup>2 - 1
    1.40 +     else (fib (n + 1))\<^sup>2 + 1)"
    1.41    by (rule fib_Cassini'_int [transferred, of n], auto)
    1.42  
    1.43