src/HOLCF/IMP/ROOT.ML
author nipkow
Mon Mar 17 15:37:41 1997 +0100 (1997-03-17)
changeset 2798 f84be65745b2
child 3663 e2d1e1151314
permissions -rw-r--r--
The HOLCF-based den. sem. of IMP.
     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 "Denotational";