--- a/src/HOL/Nat.thy Tue May 22 09:26:57 2001 +0200
+++ b/src/HOL/Nat.thy Tue May 22 15:10:06 2001 +0200
@@ -6,7 +6,7 @@
and * (for div, mod and dvd, see theory Divides).
*)
-Nat = NatDef + Inductive +
+Nat = NatDef +
(* type "nat" is a wellfounded linear order, and a datatype *)