src/HOLCF/IMP/ROOT.ML
author nipkow
Tue Sep 09 12:08:28 1997 +0200 (1997-09-09)
changeset 3663 e2d1e1151314
parent 2798 f84be65745b2
child 3954 c8c188655948
permissions -rw-r--r--
Loads HoareEx now.
     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";