src/HOL/Nat.thy

removed split_paired_Ex;
fixed proc args;

(*  Title:      HOL/Nat.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1997 TU Muenchen

Nat is a partial order
*)

Nat = NatDef +

instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)

consts
  "^"           :: ['a::power,nat] => 'a            (infixr 80)

end