|
2908
|
1 |
This directorty contains the higher order quotients in Isabelle HOL
|
|
|
2 |
|
|
|
3 |
higher order quotients use partial equivalence relations/classes (PERs)
|
|
|
4 |
instead of euivalence relations/classes
|
|
|
5 |
We have two classes er<per
|
|
|
6 |
|
|
|
7 |
Quotients are a specialization of higher order quotients.
|
|
|
8 |
The use the same constructor quot with the subclass er.
|
|
|
9 |
|
|
2910
|
10 |
An Example for the application of quotients are the fractions.
|
|
2908
|
11 |
The example shows how to define an equivalence relation and how to use
|
|
|
12 |
the quotients.
|
|
|
13 |
|
|
|
14 |
For a more detailed description see [Slo97].
|