--- a/src/HOL/UNITY/ROOT.ML Wed Oct 14 15:47:22 1998 +0200
+++ b/src/HOL/UNITY/ROOT.ML Thu Oct 15 11:35:07 1998 +0200
@@ -10,6 +10,10 @@
writeln"Root file for HOL/UNITY";
set proof_timing;
+
+loadpath := "../Lex" :: !loadpath; (*to find Prefix.thy*)
+time_use_thy"UNITY";
+
time_use_thy "Deadlock";
time_use_thy "WFair";
time_use_thy "Common";
@@ -22,9 +26,7 @@
time_use_thy "Handshake";
time_use_thy "Lift";
time_use_thy "Comp";
+time_use_thy "Client";
loadpath := "../Auth" :: !loadpath; (*to find Public.thy*)
use_thy"NSP_Bad";
-
-loadpath := "../Lex" :: !loadpath; (*to find Prefix.thy*)
-use_thy"Client";