equal
deleted
inserted
replaced
1 (* Author: Florian Haftmann, TU Muenchen *) |
1 (* Author: Florian Haftmann, TU Muenchen *) |
2 |
2 |
3 header {* Lists with elements distinct as canonical example for datatype invariants *} |
3 header {* Lists with elements distinct as canonical example for datatype invariants *} |
4 |
4 |
5 theory Dlist |
5 theory Dlist |
6 imports Main More_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 (open) 'a dlist = "{xs::'a list. distinct xs}" |
11 typedef (open) 'a dlist = "{xs::'a list. distinct xs}" |