# HG changeset patch
# User bauerg
# Date 991212539 -7200
# Node ID 6f747f6b84420fe0dd41cfc055b47d157b483519
# Parent  8ee6ed16ea452424019cd718c74ddbaf650a6bbf
injectivity of ^;

diff -r 8ee6ed16ea45 -r 6f747f6b8442 src/HOL/Power.ML
--- a/src/HOL/Power.ML	Tue May 29 11:43:12 2001 +0200
+++ b/src/HOL/Power.ML	Wed May 30 10:48:59 2001 +0200
@@ -31,6 +31,14 @@
 qed "one_le_power";
 Addsimps [one_le_power];
 
+Goal "!!i::nat. 1 < i ==> !m. (i^n = i^m) = (n=m)";
+by (induct_tac "n" 1);
+by Auto_tac;
+by (ALLGOALS (case_tac "m"));
+by Auto_tac;
+qed_spec_mp "power_inject";
+Addsimps [power_inject];
+
 Goalw [dvd_def] "!!i::nat. m<=n ==> i^m dvd i^n";
 by (etac (not_less_iff_le RS iffD2 RS add_diff_inverse RS subst) 1);
 by (asm_simp_tac (simpset() addsimps [power_add]) 1);