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.
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";