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
     3 higher order quotients use partial equivalence relations/classes (PERs) 
     4 instead of euivalence relations/classes
     5 We have two classes er<per
     7 Quotients are a specialization of higher order quotients.
     8 The use the same constructor quot with the subclass er.
    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.
    14 For a more detailed description see [Slo97].