# HG changeset patch
# User wenzelm
# Date 976134745 -3600
# Node ID 5b96bc5fbec37f44db64a30efcac7443280f11b5
# Parent  adc0ed64a120aae9686df838c456d1c55c873dde
deactivate Rational_Numbers (tmp!);

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