src/HOL/UNITY/ROOT.ML
changeset 5899 13d4753079fe
parent 5648 fe887910e32e
child 6012 1894bfc4aee9
--- a/src/HOL/UNITY/ROOT.ML	Mon Nov 16 13:58:48 1998 +0100
+++ b/src/HOL/UNITY/ROOT.ML	Mon Nov 16 13:58:56 1998 +0100
@@ -27,6 +27,7 @@
 time_use_thy "Lift";
 time_use_thy "Comp";
 time_use_thy "Client";
+time_use_thy "PPROD";
 
 loadpath := "../Auth" :: !loadpath;  (*to find Public.thy*)
 use_thy"NSP_Bad";