1
(* Title: HOL/Nat.thy
2
ID: $Id$
3
Author: Tobias Nipkow
4
Copyright 1997 TU Muenchen
5
6
Nat is a partial order
7
*)
8
9
Nat = NatDef +
10
11
instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
12
13
end