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;
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
wenzelm@3954
     7
reset global_names;
wenzelm@3954
     8
nipkow@2798
     9
(*Load theories from ../meta_theory without generating HTML files
nipkow@2798
    10
  (has already been done by HOL/IMP/ROOT.ML)*)
nipkow@2798
    11
val old_make_html = !make_html;
nipkow@2798
    12
make_html := false;
nipkow@2798
    13
loadpath := ["../../HOL/IMP"];
nipkow@2798
    14
nipkow@2798
    15
use_thy "Natural";
nipkow@2798
    16
nipkow@2798
    17
make_html := old_make_html;
nipkow@2798
    18
loadpath := ["."];
nipkow@2798
    19
nipkow@3663
    20
use_thy "HoareEx";