equal
deleted
inserted
replaced
3 *) |
3 *) |
4 |
4 |
5 header {* A variant of theory Cset from Library, defined as a quotient *} |
5 header {* A variant of theory Cset from Library, defined as a quotient *} |
6 |
6 |
7 theory Quotient_Cset |
7 theory Quotient_Cset |
8 imports "~~/src/HOL/Library/More_Set" "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Quotient_Syntax" |
8 imports Main "~~/src/HOL/Library/Quotient_Syntax" |
9 begin |
9 begin |
10 |
10 |
11 subsection {* Lifting *} |
11 subsection {* Lifting *} |
12 |
12 |
13 (*FIXME: quotient package requires a dedicated constant*) |
13 (*FIXME: quotient package requires a dedicated constant*) |