1.1 --- a/src/HOL/ex/BinEx.thy	Mon Dec 31 14:13:07 2001 +0100
     1.2 +++ b/src/HOL/ex/BinEx.thy	Wed Jan 02 16:06:31 2002 +0100
     1.3 @@ -135,6 +135,24 @@
     1.4    by simp
     1.5  
     1.6  
     1.7 +text {* \medskip Powers *}
     1.8 +
     1.9 +lemma "2 ^ 10 = (1024::int)"
    1.10 +  by simp
    1.11 +
    1.12 +lemma "-3 ^ 7 = (-2187::int)"
    1.13 +  by simp
    1.14 +
    1.15 +lemma "13 ^ 7 = (62748517::int)"
    1.16 +  by simp
    1.17 +
    1.18 +lemma "3 ^ 15 = (14348907::int)"
    1.19 +  by simp
    1.20 +
    1.21 +lemma "-5 ^ 11 = (-48828125::int)"
    1.22 +  by simp
    1.23 +
    1.24 +
    1.25  subsection {* The Natural Numbers *}
    1.26  
    1.27  text {* Successor *}
    1.28 @@ -201,6 +219,24 @@
    1.29    by simp
    1.30  
    1.31  
    1.32 +text {* \medskip Powers *}
    1.33 +
    1.34 +lemma "2 ^ 12 = (4096::nat)"
    1.35 +  by simp
    1.36 +
    1.37 +lemma "3 ^ 10 = (59049::nat)"
    1.38 +  by simp
    1.39 +
    1.40 +lemma "12 ^ 7 = (35831808::nat)"
    1.41 +  by simp
    1.42 +
    1.43 +lemma "3 ^ 14 = (4782969::nat)"
    1.44 +  by simp
    1.45 +
    1.46 +lemma "5 ^ 11 = (48828125::nat)"
    1.47 +  by simp
    1.48 +
    1.49 +
    1.50  text {* \medskip Testing the cancellation of complementary terms *}
    1.51  
    1.52  lemma "y + (x + -x) = (0::int) + y"