src/HOLCF/IMP/ROOT.ML
author nipkow
Tue, 09 Sep 1997 12:08:28 +0200
changeset 3663 e2d1e1151314
parent 2798 f84be65745b2
child 3954 c8c188655948
permissions -rw-r--r--
Loads HoareEx now.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     1
(*  Title:      HOLCF/IMP/ROOT.ML
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     2
    ID:         $Id$
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     3
    Author:     Tobias Nipkow
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     4
    Copyright   1997  TU Muenchen
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     5
*)
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     6
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     7
(*Load theories from ../meta_theory without generating HTML files
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     8
  (has already been done by HOL/IMP/ROOT.ML)*)
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     9
val old_make_html = !make_html;
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    10
make_html := false;
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    11
loadpath := ["../../HOL/IMP"];
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    12
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    13
use_thy "Natural";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    14
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    15
make_html := old_make_html;
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    16
loadpath := ["."];
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
    17
3663
e2d1e1151314 Loads HoareEx now.
nipkow
parents: 2798
diff changeset
    18
use_thy "HoareEx";