# HG changeset patch
# User wenzelm
# Date 976720930 -3600
# Node ID cd07dd2ccd36bc63baa92e60bd4f0bcce8f42352
# Parent  da5373fa06dea7c905d9c3125bafdb3f085e354d
tuned comments;

diff -r da5373fa06de -r cd07dd2ccd36 src/HOL/Library/Rational_Numbers.thy
--- 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)"