author | haftmann |
Tue, 28 Apr 2009 16:58:23 +0200 | |
changeset 31019 | 0a38079e789b |
parent 31018 | b8a8cf6e16f2 |
child 31020 | 9999a77590c3 |
1.1 --- a/src/HOL/NSA/NSComplex.thy Tue Apr 28 15:50:32 2009 +0200 1.2 +++ b/src/HOL/NSA/NSComplex.thy Tue Apr 28 16:58:23 2009 +0200 1.3 @@ -383,7 +383,7 @@ 1.4 by transfer (rule power_mult_distrib) 1.5 1.6 lemma hcpow_zero2 [simp]: 1.7 - "\<And>n. 0 pow (hSuc n) = (0::'a::{semiring_0} star)" 1.8 + "\<And>n. 0 pow (hSuc n) = (0::'a::{power,semiring_0} star)" 1.9 by transfer (rule power_0_Suc) 1.10 1.11 lemma hcpow_not_zero [simp,intro]: