--- a/src/HOL/Complex/NSInduct.thy Sat Feb 14 02:06:12 2004 +0100
+++ b/src/HOL/Complex/NSInduct.thy Sun Feb 15 10:46:37 2004 +0100
@@ -4,7 +4,7 @@
Description: Nonstandard characterization of induction etc.
*)
-NSInduct = ComplexArith0 +
+NSInduct = Complex +
constdefs