# HG changeset patch
# User paulson
# Date 961749291 -7200
# Node ID 44fc37919579feddee2ca927f4a87dc4f9f9c7f9
# Parent  33b32680669a250a1ce6737852606722f6e40c95
added the AllocImpl example

diff -r 33b32680669a -r 44fc37919579 src/HOL/UNITY/ROOT.ML
--- a/src/HOL/UNITY/ROOT.ML	Fri Jun 23 10:34:31 2000 +0200
+++ b/src/HOL/UNITY/ROOT.ML	Fri Jun 23 10:34:51 2000 +0200
@@ -20,10 +20,14 @@
 time_use_thy "Lift";
 time_use_thy "Comp";
 time_use_thy "Reachability";
+
 (*Allocator example*)
 time_use_thy "PPROD";
 time_use_thy "TimerArray";
-with_path "../Induct" time_use_thy "Alloc";
+
+add_path "../Induct";
+time_use_thy "Alloc";
+time_use_thy "AllocImpl";
 time_use_thy "Client";
 
 time_use_thy "ELT";  (*obsolete*)