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