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