equal
deleted
inserted
replaced
1 (* Title: HOL/Quotient_Examples/Lift_DList.thy |
1 (* Title: HOL/Quotient_Examples/Lift_DList.thy |
2 Author: Ondrej Kuncar |
2 Author: Ondrej Kuncar |
3 *) |
3 *) |
4 |
4 |
5 theory Lift_DList |
5 theory Lift_DList |
6 imports Main "~~/src/HOL/Library/Quotient_List" |
6 imports Main |
7 begin |
7 begin |
8 |
8 |
9 subsection {* The type of distinct lists *} |
9 subsection {* The type of distinct lists *} |
10 |
10 |
11 typedef 'a dlist = "{xs::'a list. distinct xs}" |
11 typedef 'a dlist = "{xs::'a list. distinct xs}" |