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";