# HG changeset patch
# User haftmann
# Date 1265981281 -3600
# Node ID 36c0a6dd8c6fd2a0f918143b341ebfe96142f7fc
# Parent  0a3adceb9c6709cea52b3de2c52f8b55d30ad28e
tuned import order

diff -r 0a3adceb9c67 -r 36c0a6dd8c6f src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Fri Feb 12 09:49:28 2010 +0100
+++ b/src/HOL/Lattices.thy	Fri Feb 12 14:28:01 2010 +0100
@@ -5,7 +5,7 @@
 header {* Abstract lattices *}
 
 theory Lattices
-imports Orderings
+imports Orderings Groups
 begin
 
 subsection {* Lattices *}
diff -r 0a3adceb9c67 -r 36c0a6dd8c6f src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Fri Feb 12 09:49:28 2010 +0100
+++ b/src/HOL/Nat.thy	Fri Feb 12 14:28:01 2010 +0100
@@ -8,7 +8,7 @@
 header {* Natural numbers *}
 
 theory Nat
-imports Inductive Product_Type Fields
+imports Inductive Typedef Fun Fields
 uses
   "~~/src/Tools/rat.ML"
   "~~/src/Provers/Arith/cancel_sums.ML"