equal
deleted
inserted
replaced
3 Author: Oscar Slotosch and Markus Wenzel, TU Muenchen |
3 Author: Oscar Slotosch and Markus Wenzel, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 header {* Partial equivalence relations *} |
6 header {* Partial equivalence relations *} |
7 |
7 |
8 theory PER = Main: |
8 theory PER imports Main begin |
9 |
9 |
10 text {* |
10 text {* |
11 Higher-order quotients are defined over partial equivalence |
11 Higher-order quotients are defined over partial equivalence |
12 relations (PERs) instead of total ones. We provide axiomatic type |
12 relations (PERs) instead of total ones. We provide axiomatic type |
13 classes @{text "equiv < partial_equiv"} and a type constructor |
13 classes @{text "equiv < partial_equiv"} and a type constructor |