src/HOLCF/IMP/ROOT.ML
changeset 6217 9dac1ee185e3
parent 5210 54aaa779b6b4
child 6488 271969bb7f95
     1.1 --- a/src/HOLCF/IMP/ROOT.ML	Wed Feb 03 17:34:27 1999 +0100
     1.2 +++ b/src/HOLCF/IMP/ROOT.ML	Wed Feb 03 17:36:55 1999 +0100
     1.3 @@ -4,15 +4,8 @@
     1.4      Copyright   1997  TU Muenchen
     1.5  *)
     1.6  
     1.7 -(*Load theories from ../meta_theory without generating HTML files
     1.8 -  (has already been done by HOL/IMP/ROOT.ML)*)
     1.9 -val old_make_html = !make_html;
    1.10 -make_html := false;
    1.11 -loadpath := ["../../HOL/IMP"];
    1.12 -
    1.13 +add_path "../../HOL/IMP";
    1.14  use_thy "Natural";
    1.15  
    1.16 -make_html := old_make_html;
    1.17 -loadpath := ["."];
    1.18 -
    1.19 +reset_path ();
    1.20  use_thy "HoareEx";