--- 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 *}
--- 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"