src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Thu Feb 15 16:00:35 2001 +0100
+++ b/src/HOL/Nat.thy	Thu Feb 15 16:00:36 2001 +0100
@@ -8,7 +8,7 @@
 
 Nat = NatDef + Inductive +
 
-(* type "nat" is a linear order, and a datatype *)
+(* type "nat" is a wellfounded linear order, and a datatype *)
 
 rep_datatype nat
   distinct Suc_not_Zero, Zero_not_Suc
@@ -17,6 +17,7 @@
 
 instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
 instance nat :: linorder (nat_le_linear)
+instance nat :: wellorder (wf_less)
 
 axclass power < term