| changeset 25691 | 8f8d83af100a |
| parent 25594 | 43c718438f9f |
| child 27368 | 9f90ac19e32b |
--- a/src/HOL/Library/Continuity.thy Tue Dec 18 12:26:24 2007 +0100 +++ b/src/HOL/Library/Continuity.thy Tue Dec 18 14:37:00 2007 +0100 @@ -6,7 +6,7 @@ header {* Continuity and iterations (of set transformers) *} theory Continuity -imports PreList +imports ATP_Linkup begin subsection {* Continuity for complete lattices *}