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.
added nat as instance of new wellorder axclass
authoroheimb
Thu, 15 Feb 2001 16:00:36 +0100
changeset 11134 8bc06c4202cd
parent 11133 7c66f3dc7d14
child 11135 8fd0dea26286
added nat as instance of new wellorder axclass
src/HOL/Nat.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle