Added lemmas to Ring_and_Field with slightly modified simplification rules
Deleted some little-used integer theorems, replacing them by the generic ones
in Ring_and_Field
Consolidated integer powers
(* Title: HOL/Lattice/ROOT.ML
ID: $Id$
Author: Markus Wenzel, TU Muenchen
Basic theory of lattices and orders.
*)
time_use_thy "CompleteLattice";