src/HOL/Quot/README
changeset 2910 905aa895136c
parent 2908 b9ba893e72cd
equal deleted inserted replaced
2909:22a8a97b66be 2910:905aa895136c
     5 We have two classes er<per
     5 We have two classes er<per
     6 
     6 
     7 Quotients are a specialization of higher order quotients.
     7 Quotients are a specialization of higher order quotients.
     8 The use the same constructor quot with the subclass er.
     8 The use the same constructor quot with the subclass er.
     9 
     9 
    10 An Example for the application of quotients are the fractional numbers.
    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
    11 The example shows how to define an equivalence relation and how to use
    12 the quotients.
    12 the quotients.
    13 
    13 
    14 For a more detailed description see [Slo97].
    14 For a more detailed description see [Slo97].