src/HOL/Lfp.thy
changeset 15131 c69542757a4d
parent 14169 0590de71a016
child 15140 322485b816ac
--- a/src/HOL/Lfp.thy	Mon Aug 16 14:21:54 2004 +0200
+++ b/src/HOL/Lfp.thy	Mon Aug 16 14:22:27 2004 +0200
@@ -6,7 +6,9 @@
 The Knaster-Tarski Theorem
 *)
 
-theory Lfp = Product_Type:
+theory Lfp
+import Product_Type
+begin
 
 constdefs
   lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set"