# HG changeset patch
# User paulson
# Date 959357218 -7200
# Node ID 718907f55f62ce7f67f40f888651cd7f3dde8e39
# Parent  8b7718296a35b390af54f1878bdcccaa15006166
fixed the dependences

diff -r 8b7718296a35 -r 718907f55f62 src/HOL/UNITY/ROOT.ML
--- a/src/HOL/UNITY/ROOT.ML	Fri May 26 18:06:43 2000 +0200
+++ b/src/HOL/UNITY/ROOT.ML	Fri May 26 18:06:58 2000 +0200
@@ -23,13 +23,14 @@
 time_use_thy "Handshake";
 time_use_thy "Lift";
 time_use_thy "Comp";
+time_use_thy "Reachability";
 (*Allocator example*)
-time_use_thy "Client";
-time_use_thy "ELT";  (*obsolete*)
 time_use_thy "PPROD";
 time_use_thy "TimerArray";
-time_use_thy "Alloc";
-time_use_thy "Reachability";
+with_path "../Induct" time_use_thy "Alloc";
+time_use_thy "Client";
+
+time_use_thy "ELT";  (*obsolete*)
 
 add_path "../Auth";	(*to find Public.thy*)
 use_thy"NSP_Bad";