# HG changeset patch
# User paulson
# Date 849096067 -3600
# Node ID 187d001fbe797aa1cfd7577506222097b1068c09
# Parent  d388a38f7198ae6d7508163b51230c70c501037b
Better indentation

diff -r d388a38f7198 -r 187d001fbe79 src/ZF/ex/ROOT.ML
--- a/src/ZF/ex/ROOT.ML	Wed Nov 27 12:59:12 1996 +0100
+++ b/src/ZF/ex/ROOT.ML	Wed Nov 27 13:01:07 1996 +0100
@@ -12,9 +12,9 @@
 proof_timing := true;
 
 time_use     "misc.ML";
-time_use_thy "Primes";		(*GCD theory*)
-time_use_thy "Ramsey";		(*Simple form of Ramsey's theorem*)
-time_use_thy "Limit";		(*Inverse limit construction of domains*)
+time_use_thy "Primes";          (*GCD theory*)
+time_use_thy "Ramsey";          (*Simple form of Ramsey's theorem*)
+time_use_thy "Limit";           (*Inverse limit construction of domains*)
 
 (*Integers & Binary integer arithmetic*)
 time_use_thy "Bin";