diff -r cb82606b8215 -r 3fbcfa911863 src/HOL/Quotient_Examples/Lift_DList.thy --- a/src/HOL/Quotient_Examples/Lift_DList.thy Tue Aug 13 15:59:22 2013 +0200 +++ b/src/HOL/Quotient_Examples/Lift_DList.thy Tue Aug 13 15:59:22 2013 +0200 @@ -3,7 +3,7 @@ *) theory Lift_DList -imports Main "~~/src/HOL/Library/Quotient_List" +imports Main begin subsection {* The type of distinct lists *}