# HG changeset patch
# User slotosch
# Date 860162628 -7200
# Node ID b9ba893e72cd77835ed2f0763bc8f373ddf2555c
# Parent  0e272e4c7cb254f4c13bd4fc2f2d9774ba3716d0
Start Example

diff -r 0e272e4c7cb2 -r b9ba893e72cd src/HOL/Quot/README
--- 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].
diff -r 0e272e4c7cb2 -r b9ba893e72cd src/HOL/Quot/ROOT.ML
--- a/src/HOL/Quot/ROOT.ML	Fri Apr 04 16:03:44 1997 +0200
+++ b/src/HOL/Quot/ROOT.ML	Fri Apr 04 16:03:48 1997 +0200
@@ -10,5 +10,5 @@
 
 writeln"Root file for HOL/Quot";
 
-(*use_thy "Quot";*)
+use_thy "FRACT";