Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
simpliefied instance statement
authorhaftmann
Wed, 14 Feb 2007 10:06:14 +0100
changeset 22318 6efe70ab7add
parent 22317 b550d2c6ca90
child 22319 6f162dd72f60
simpliefied instance statement
src/HOL/Nat.thy file | annotate | diff | comparison | revisions 
--- 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)+
isabelle