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

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

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