# HG changeset patch
# User wenzelm
# Date 981312212 -3600
# Node ID 32a98609ce921ed34145f1729b684be66494efb8
# Parent  b84dd2c25a1c0be6f1c62ddf7bbec3a5eb5fbf99
tuned

diff -r b84dd2c25a1c -r 32a98609ce92 src/HOL/Library/ROOT.ML
--- a/src/HOL/Library/ROOT.ML	Sun Feb 04 19:43:15 2001 +0100
+++ b/src/HOL/Library/ROOT.ML	Sun Feb 04 19:43:32 2001 +0100
@@ -1,1 +1,2 @@
+
 use_thy "Library";