src/HOL/UNITY/ROOT.ML
changeset 5620 3ac11c4af76a
parent 5430 4a179dba527a
child 5638 2570d7c3f6e7
     1.1 --- a/src/HOL/UNITY/ROOT.ML	Wed Oct 07 10:31:30 1998 +0200
     1.2 +++ b/src/HOL/UNITY/ROOT.ML	Wed Oct 07 10:32:00 1998 +0200
     1.3 @@ -21,6 +21,12 @@
     1.4  time_use_thy "Reach";
     1.5  time_use_thy "Handshake";
     1.6  time_use_thy "Lift";
     1.7 +time_use_thy "Comp";
     1.8  
     1.9 -loadpath := "../Auth" :: !loadpath;  (*necessary to find the Auth theories*)
    1.10 +loadpath := "../Auth" :: !loadpath;  (*to find Public.thy*)
    1.11  use_thy"NSP_Bad";
    1.12 +
    1.13 +(*
    1.14 +loadpath := "../Lex" :: !loadpath;   (*to find Prefix.thy*)
    1.15 +use_thy"Client";
    1.16 +*)