src/HOL/Fun.thy
changeset 44860 56101fa00193
parent 44744 bdf8eb8f126b
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Fun.thy	Sat Sep 10 00:44:25 2011 +0200
     1.2 +++ b/src/HOL/Fun.thy	Sat Sep 10 10:29:24 2011 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Notions about functions *}
     1.5  
     1.6  theory Fun
     1.7 -imports Complete_Lattice
     1.8 +imports Complete_Lattices
     1.9  uses ("Tools/enriched_type.ML")
    1.10  begin
    1.11