Better indentation
authorpaulson
Wed, 27 Nov 1996 13:01:07 +0100
changeset 2248 187d001fbe79
parent 2247 d388a38f7198
child 2249 2af17dd5479e
Better indentation
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";