# HG changeset patch
# User paulson
# Date 957446178 -7200
# Node ID 59a4b5e6a591c5ebbe20f8bc826931cb6580b1fc
# Parent  50b650d1964106cbe67a0b7e0bd6d565bc392eac
new lemmas concerning powers and #mmm

diff -r 50b650d19641 -r 59a4b5e6a591 src/HOL/Integ/NatBin.ML
--- a/src/HOL/Integ/NatBin.ML	Thu May 04 15:15:37 2000 +0200
+++ b/src/HOL/Integ/NatBin.ML	Thu May 04 15:16:18 2000 +0200
@@ -373,7 +373,15 @@
 Goal "(p::nat) ^ #0 = #1";
 by (simp_tac numeral_ss 1);
 qed "power_zero";
-Addsimps [power_zero];
+
+Goal "(p::nat) ^ #1 = p";
+by (simp_tac numeral_ss 1);
+qed "power_one";
+Addsimps [power_zero, power_one];
+
+Goal "(p::nat) ^ #2 = p*p";
+by (simp_tac numeral_ss 1);
+qed "power_two";
 
 val binomial_zero = rename_numerals thy binomial_0;
 val binomial_Suc' = rename_numerals thy binomial_Suc;
@@ -383,6 +391,7 @@
 Addsimps (map (rename_numerals thy) 
 	  [binomial_n_0, binomial_zero, binomial_1]);
 
+Addsimps [rename_numerals thy card_Pow];
 
 (*** Comparisons involving 0 ***)