src/HOL/Nat.thy
author nipkow
Wed Feb 12 18:53:59 1997 +0100 (1997-02-12)
changeset 2608 450c9b682a92
parent 2541 70aa00ed3025
child 3370 5c5fdce3a4e4
permissions -rw-r--r--
New class "order" and accompanying changes.
In particular reflexivity of <= is now one rewrite rule.
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