src/HOL/Algebra/ROOT.ML

--- a/src/HOL/Algebra/ROOT.ML	Tue Apr 13 07:48:32 2004 +0200
+++ b/src/HOL/Algebra/ROOT.ML	Tue Apr 13 09:42:40 2004 +0200
@@ -16,6 +16,7 @@
 use_thy "FiniteProduct";	(* Product operator for commutative groups *)
 use_thy "Sylow";		(* Sylow's theorem *)
 use_thy "Bij";			(* Automorphism Groups *)
+use_thy "Lattice";              (* Lattices, and the complete lattice of subgroups *)
 
 (* Rings *)