src/HOL/MiniML/ROOT.ML
changeset 2031 03a843f0f447
parent 1925 1150f128c7fe
child 2525 477c05586286
--- a/src/HOL/MiniML/ROOT.ML	Thu Sep 26 11:11:22 1996 +0200
+++ b/src/HOL/MiniML/ROOT.ML	Thu Sep 26 12:47:47 1996 +0200
@@ -1,12 +1,12 @@
-(*  Title: 	HOL/MiniML/ROOT.ML
+(*  Title:      HOL/MiniML/ROOT.ML
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1995 TUM
 
 Type inference for let-free MiniML
 *)
 
-HOL_build_completed;	(*Make examples fail if HOL did*)
+HOL_build_completed;    (*Make examples fail if HOL did*)
 
 writeln"Root file for HOL/MiniML";
 Unify.trace_bound := 20;