src/HOLCF/IMP/ROOT.ML
author wenzelm
Tue Jul 28 17:05:34 1998 +0200 (1998-07-28)
changeset 5210 54aaa779b6b4
parent 3954 c8c188655948
child 6217 9dac1ee185e3
permissions -rw-r--r--
removed global_names flag;
     1 (*  Title:      HOLCF/IMP/ROOT.ML
     2     ID:         $Id$
     3     Author:     Tobias Nipkow
     4     Copyright   1997  TU Muenchen
     5 *)
     6 
     7 (*Load theories from ../meta_theory without generating HTML files
     8   (has already been done by HOL/IMP/ROOT.ML)*)
     9 val old_make_html = !make_html;
    10 make_html := false;
    11 loadpath := ["../../HOL/IMP"];
    12 
    13 use_thy "Natural";
    14 
    15 make_html := old_make_html;
    16 loadpath := ["."];
    17 
    18 use_thy "HoareEx";