# HG changeset patch
# User wenzelm
# Date 976135969 -3600
# Node ID 0cf191f57a54d64e892c7bb669d5e0e1808157a2
# Parent  5b96bc5fbec37f44db64a30efcac7443280f11b5
activate Rational_Numbers;

diff -r 5b96bc5fbec3 -r 0cf191f57a54 src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Wed Dec 06 21:32:25 2000 +0100
+++ b/src/HOL/Library/Library.thy	Wed Dec 06 21:52:49 2000 +0100
@@ -2,7 +2,7 @@
 theory Library =
   Quotient +
   Ring_and_Field +
-(*  Rational_Numbers +  *)
+  Rational_Numbers +
   List_Prefix +
   Accessible_Part +
   Multiset +