# HG changeset patch
# User haftmann
# Date 1171443974 -3600
# Node ID 6efe70ab7add2f7f4ccdb527028d72ca5436f1e1
# Parent  b550d2c6ca901caaa523d719ad0de11db1b4eedb
simpliefied instance statement

diff -r b550d2c6ca90 -r 6efe70ab7add src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Feb 14 10:06:13 2007 +0100
+++ b/src/HOL/Nat.thy	Wed Feb 14 10:06:14 2007 +0100
@@ -439,7 +439,7 @@
 
 text {* Type {@typ nat} is a wellfounded linear order *}
 
-instance nat :: "{order, linorder, wellorder}"
+instance nat :: wellorder
   by intro_classes
     (assumption |
       rule le_refl le_trans le_anti_sym nat_less_le nat_le_linear wf_less)+