summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | slotosch |

Fri, 04 Apr 1997 16:03:48 +0200 | |

changeset 2908 | b9ba893e72cd |

parent 2907 | 0e272e4c7cb2 |

child 2909 | 22a8a97b66be |

Start Example

src/HOL/Quot/README | file | annotate | diff | comparison | revisions | |

src/HOL/Quot/ROOT.ML | file | annotate | diff | comparison | revisions |

--- a/src/HOL/Quot/README Fri Apr 04 16:03:44 1997 +0200 +++ b/src/HOL/Quot/README Fri Apr 04 16:03:48 1997 +0200 @@ -0,0 +1,14 @@ +This directorty contains the higher order quotients in Isabelle HOL + +higher order quotients use partial equivalence relations/classes (PERs) +instead of euivalence relations/classes +We have two classes er<per + +Quotients are a specialization of higher order quotients. +The use the same constructor quot with the subclass er. + +An Example for the application of quotients are the fractional numbers. +The example shows how to define an equivalence relation and how to use +the quotients. + +For a more detailed description see [Slo97].