| changeset 53013 | 3fbcfa911863 |
| parent 49834 | b27bbb021df1 |
| child 55524 | f41ef840f09d |
--- 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 *}