src/HOL/LOrder.thy

--- a/src/HOL/LOrder.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/LOrder.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -5,7 +5,9 @@
 
 header {* Lattice Orders *}
 
-theory LOrder = HOL:
+theory LOrder
+import HOL
+begin
 
 text {*
   The theory of lattices developed here is taken from the book:
@@ -327,4 +329,4 @@
 val modular_le = thm "modular_le";
 *}
 
-end
\ No newline at end of file
+end