src/HOLCF/IOA/Modelcheck/ROOT.ML
author wenzelm
Thu Apr 22 18:20:37 1999 +0200 (1999-04-22)
changeset 6488 271969bb7f95
parent 6471 08d12ef5fc19
child 7299 743b22579a2f
permissions -rw-r--r--
more graceful handling of load paths;
wenzelm@6488
     1
(*  Title:      HOLCF/IOA/Modelcheck/ROOT.ML
mueller@6471
     2
    ID:         $Id$
mueller@6471
     3
    Author:     Olaf Mueller
mueller@6471
     4
    Copyright   1997  TU Muenchen
mueller@6471
     5
mueller@6471
     6
This is the ROOT file for the formalization of a semantic model of
mueller@6471
     7
I/O-Automata.  See the README.html file for details.
mueller@6471
     8
*)
mueller@6471
     9
mueller@6471
    10
goals_limit := 1;
mueller@6471
    11
wenzelm@6488
    12
use "../../../HOL/Modelcheck/mucke_oracle.ML";
wenzelm@6488
    13
use_thy "../../../HOL/Modelcheck/MuckeSyn";
wenzelm@6488
    14
use_thy "MuIOAOracle";
wenzelm@6488
    15
use_thy "Cockpit";
wenzelm@6488
    16
use_thy "Ring3";