# HG changeset patch
# User wenzelm
# Date 974483253 -3600
# Node ID 9efb2fd5399ebdde249dbe1d8534d0357d2593dc
# Parent  76dedf65408f9b253f0c759c565a0c13ae687963
Ring_and_Field;

diff -r 76dedf65408f -r 9efb2fd5399e src/HOL/Library/Library.thy
--- a/src/HOL/Library/Library.thy	Fri Nov 17 18:47:15 2000 +0100
+++ b/src/HOL/Library/Library.thy	Fri Nov 17 18:47:33 2000 +0100
@@ -2,6 +2,7 @@
 theory Library =
   List_Prefix +
   Quotient +
+  Ring_and_Field +
   Accessible_Part +
   Multiset +
   While_Combinator + While_Combinator_Example: