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