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].