--- a/src/HOL/Real/PRat.thy Wed May 10 21:04:16 2000 +0200
+++ b/src/HOL/Real/PRat.thy Wed May 10 22:34:30 2000 +0200
@@ -5,7 +5,7 @@
Description : The positive rationals
*)
-PRat = PNat + Equiv +
+PRat = PNat +
constdefs
ratrel :: "((pnat * pnat) * (pnat * pnat)) set"