| changeset 41477 | be6d903e5943 |
| parent 41436 | 480978f80eae |
| child 41533 | 869b5ea478b0 |
--- a/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sat Jan 08 09:30:52 2011 -0800 +++ b/src/HOL/HOLCF/Library/Defl_Bifinite.thy Sat Jan 08 09:34:08 2011 -0800 @@ -5,7 +5,7 @@ header {* Algebraic deflations are a bifinite domain *} theory Defl_Bifinite -imports HOLCF Infinite_Set +imports HOLCF "~~/src/HOL/Library/Infinite_Set" begin subsection {* Lemmas about MOST *}