src/HOL/Fun.thy
changeset 32139 e271a64f03ff
parent 31949 3f933687fae9
child 32337 7887cb2848bb
--- a/src/HOL/Fun.thy	Wed Jul 22 14:21:52 2009 +0200
+++ b/src/HOL/Fun.thy	Wed Jul 22 18:02:10 2009 +0200
@@ -6,7 +6,7 @@
 header {* Notions about functions *}
 
 theory Fun
-imports Set
+imports Complete_Lattice
 begin
 
 text{*As a simplification rule, it replaces all function equalities by