Deleted option_case_tac because exhaust_tac performs a similar function.
Deleted the duplicate proof of expand_option_case...
(* 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)
end