| changeset 45990 | b7b905b23b2a |
| parent 45129 | 1fce03e3e8ad |
| child 47092 | fa3538d6004b |
--- a/src/HOL/Quotient_Examples/DList.thy Mon Dec 26 22:17:10 2011 +0100 +++ b/src/HOL/Quotient_Examples/DList.thy Mon Dec 26 22:17:10 2011 +0100 @@ -8,7 +8,7 @@ header {* Lists with distinct elements *} theory DList -imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List" +imports "~~/src/HOL/Library/Quotient_List" begin text {* Some facts about lists *}