src/HOL/Nat.thy
author nipkow
Tue Apr 08 10:48:42 1997 +0200 (1997-04-08)
changeset 2919 953a47dc0519
parent 2608 450c9b682a92
child 3370 5c5fdce3a4e4
permissions -rw-r--r--
Dep. on Provers/nat_transitive
clasohm@923
     1
(*  Title:      HOL/Nat.thy
clasohm@923
     2
    ID:         $Id$
nipkow@2608
     3
    Author:     Tobias Nipkow
nipkow@2608
     4
    Copyright   1997 TU Muenchen
clasohm@923
     5
nipkow@2608
     6
Nat is a partial order
clasohm@923
     7
*)
clasohm@923
     8
nipkow@2608
     9
Nat = NatDef +
clasohm@923
    10
nipkow@2608
    11
instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
oheimb@1660
    12
clasohm@923
    13
end