--- a/src/HOL/Library/Rational_Numbers.thy Wed Dec 13 16:21:40 2000 +0100
+++ b/src/HOL/Library/Rational_Numbers.thy Wed Dec 13 16:22:10 2000 +0100
@@ -623,10 +623,10 @@
subsection {* Embedding integers *}
-constdefs (* FIXME generalize int to any numeric subtype *)
- rat :: "int => rat"
+constdefs
+ rat :: "int => rat" (* FIXME generalize int to any numeric subtype *)
"rat z == Fract z #1"
- int_set :: "rat set" ("\<int>")
+ int_set :: "rat set" ("\<int>") (* FIXME generalize rat to any numeric supertype *)
"\<int> == range rat"
lemma rat_inject: "(rat z = rat w) = (z = w)"