src/HOL/UNITY/ROOT.ML
changeset 8128 3a5864b465e2
parent 7513 879ae27f5e6f
child 8251 9be357df93d4
--- a/src/HOL/UNITY/ROOT.ML	Thu Jan 13 17:36:58 2000 +0100
+++ b/src/HOL/UNITY/ROOT.ML	Fri Jan 14 12:17:53 2000 +0100
@@ -28,7 +28,7 @@
 time_use_thy "Extend";
 time_use_thy "PPROD";
 time_use_thy "TimerArray";
-time_use_thy "Follows";
+time_use_thy "Alloc";
 
 add_path "../Auth";	(*to find Public.thy*)
 use_thy"NSP_Bad";