src/HOL/Quot/README
author paulson
Thu Sep 23 13:06:31 1999 +0200 (1999-09-23)
changeset 7584 5be4bb8e4e3f
parent 2910 905aa895136c
permissions -rw-r--r--
tidied; added lemma restrict_to_left
     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 
    10 An Example for the application of quotients are the fractions.
    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].