author | huffman |
Sat, 08 Jan 2011 09:34:08 -0800 | |
changeset 41477 | be6d903e5943 |
parent 41476 | 0fa9629aa399 |
child 41478 | 18500bd1f47b |
--- 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 *}