# HG changeset patch
# User haftmann
# Date 1240930703 -7200
# Node ID 0a38079e789b1f1aafbbad342e7034e25012fedb
# Parent  b8a8cf6e16f212995db33a331b9dbbf2f616ed23
power constraint needed, though

diff -r b8a8cf6e16f2 -r 0a38079e789b src/HOL/NSA/NSComplex.thy
--- a/src/HOL/NSA/NSComplex.thy	Tue Apr 28 15:50:32 2009 +0200
+++ b/src/HOL/NSA/NSComplex.thy	Tue Apr 28 16:58:23 2009 +0200
@@ -383,7 +383,7 @@
 by transfer (rule power_mult_distrib)
 
 lemma hcpow_zero2 [simp]:
-  "\<And>n. 0 pow (hSuc n) = (0::'a::{semiring_0} star)"
+  "\<And>n. 0 pow (hSuc n) = (0::'a::{power,semiring_0} star)"
 by transfer (rule power_0_Suc)
 
 lemma hcpow_not_zero [simp,intro]: