src/HOLCF/IMP/ROOT.ML
author wenzelm
Wed, 03 Feb 1999 17:36:55 +0100 (1999-02-03)
changeset 6217 9dac1ee185e3
parent 5210 54aaa779b6b4
child 6488 271969bb7f95
permissions -rw-r--r--
tidied load path handling;
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
6217
9dac1ee185e3 tidied load path handling;
wenzelm
parents: 5210
diff changeset
     7
add_path "../../HOL/IMP";
2798
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     8
use_thy "Natural";
f84be65745b2 The HOLCF-based den. sem. of IMP.
nipkow
parents:
diff changeset
     9
6217
9dac1ee185e3 tidied load path handling;
wenzelm
parents: 5210
diff changeset
    10
reset_path ();
3663
e2d1e1151314 Loads HoareEx now.
nipkow
parents: 2798
diff changeset
    11
use_thy "HoareEx";