# HG changeset patch
# User wenzelm
# Date 974483235 -3600
# Node ID 76dedf65408f9b253f0c759c565a0c13ae687963
# Parent  e7a5e8d63394b1f3a7545033dd2876e116a0b9db
Library/Ring_and_Field.thy;

diff -r e7a5e8d63394 -r 76dedf65408f src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Nov 16 23:12:58 2000 +0100
+++ b/src/HOL/IsaMakefile	Fri Nov 17 18:47:15 2000 +0100
@@ -163,8 +163,9 @@
 
 $(LOG)/HOL-Library.gz: $(OUT)/HOL Library/Accessible_Part.thy \
   Library/Library.thy Library/List_Prefix.thy Library/Multiset.thy \
-  Library/Quotient.thy Library/README.html Library/ROOT.ML \
-  Library/While_Combinator.thy Library/While_Combinator_Example.thy
+  Library/Quotient.thy Library/Ring_and_Field.thy Library/README.html \
+  Library/ROOT.ML Library/While_Combinator.thy \
+  Library/While_Combinator_Example.thy
 	@$(ISATOOL) usedir $(OUT)/HOL Library