1132 introduced most of the abstract notions about quotients and also deals with |
1132 introduced most of the abstract notions about quotients and also deals with |
1133 lifting of higher-order theorems. However, he cannot deal with quotient |
1133 lifting of higher-order theorems. However, he cannot deal with quotient |
1134 compositions (needed for lifting theorems about @{text flat}). Also, a |
1134 compositions (needed for lifting theorems about @{text flat}). Also, a |
1135 number of his definitions, like @{text ABS}, @{text REP} and @{text INJ} etc |
1135 number of his definitions, like @{text ABS}, @{text REP} and @{text INJ} etc |
1136 only exist in \cite{Homeier05} as ML-code, not included in the paper. |
1136 only exist in \cite{Homeier05} as ML-code, not included in the paper. |
|
1137 Like Homeier's, our quotient package can deal with partial equivalence |
|
1138 relations, but for lack of space we do not describe the mechanisms |
|
1139 needed for this kind of quotient constructions. |
1137 |
1140 |
1138 |
1141 |
1139 One feature of our quotient package is that when lifting theorems, the user |
1142 One feature of our quotient package is that when lifting theorems, the user |
1140 can precisely specify what the lifted theorem should look like. This feature |
1143 can precisely specify what the lifted theorem should look like. This feature |
1141 is necessary, for example, when lifting an induction principle for two |
1144 is necessary, for example, when lifting an induction principle for two |