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;
nipkow@2798
     1
(*  Title:      HOLCF/IMP/ROOT.ML
nipkow@2798
     2
    ID:         $Id$
nipkow@2798
     3
    Author:     Tobias Nipkow
nipkow@2798
     4
    Copyright   1997  TU Muenchen
nipkow@2798
     5
*)
nipkow@2798
     6
nipkow@2798
     7
(*Load theories from ../meta_theory without generating HTML files
nipkow@2798
     8
  (has already been done by HOL/IMP/ROOT.ML)*)
nipkow@2798
     9
val old_make_html = !make_html;
nipkow@2798
    10
make_html := false;
nipkow@2798
    11
loadpath := ["../../HOL/IMP"];
nipkow@2798
    12
nipkow@2798
    13
use_thy "Natural";
nipkow@2798
    14
nipkow@2798
    15
make_html := old_make_html;
nipkow@2798
    16
loadpath := ["."];
nipkow@2798
    17
nipkow@3663
    18
use_thy "HoareEx";