src/HOL/Auth/ROOT.ML

--- a/src/HOL/Auth/ROOT.ML	Thu Mar 11 12:34:10 1999 +0100
+++ b/src/HOL/Auth/ROOT.ML	Thu Mar 11 13:20:35 1999 +0100
@@ -6,9 +6,8 @@
 Root file for protocol proofs.
 *)
 
-HOL_build_completed;    (*Make examples fail if HOL did*)
+writeln"Root file for HOL/Auth";
 
-writeln"Root file for HOL/Auth";
 set proof_timing;
 goals_limit := 1;
 HOL_quantifiers := false;
@@ -28,4 +27,3 @@
 time_use_thy "NS_Public_Bad";
 time_use_thy "NS_Public";
 time_use_thy "TLS";
-