src/HOL/Fun.thy
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15303 eedbb8d22ca2
--- a/src/HOL/Fun.thy	Tue Aug 17 11:00:24 2004 +0200
+++ b/src/HOL/Fun.thy	Wed Aug 18 11:09:40 2004 +0200
@@ -7,7 +7,7 @@
 *)
 
 theory Fun 
-import Typedef
+imports Typedef
 begin
 
 instance set :: (type) order