summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Quot/README

changeset 2908 | b9ba893e72cd |

parent 2898 | d7bff1252d1e |

child 2910 | 905aa895136c |

1.1 --- a/src/HOL/Quot/README Fri Apr 04 16:03:44 1997 +0200 1.2 +++ b/src/HOL/Quot/README Fri Apr 04 16:03:48 1997 +0200 1.3 @@ -0,0 +1,14 @@ 1.4 +This directorty contains the higher order quotients in Isabelle HOL 1.5 + 1.6 +higher order quotients use partial equivalence relations/classes (PERs) 1.7 +instead of euivalence relations/classes 1.8 +We have two classes er<per 1.9 + 1.10 +Quotients are a specialization of higher order quotients. 1.11 +The use the same constructor quot with the subclass er. 1.12 + 1.13 +An Example for the application of quotients are the fractional numbers. 1.14 +The example shows how to define an equivalence relation and how to use 1.15 +the quotients. 1.16 + 1.17 +For a more detailed description see [Slo97].