src/HOLCF/IOA/Modelcheck/ROOT.ML
author mueller
Thu Apr 22 11:09:05 1999 +0200 (1999-04-22)
changeset 6471 08d12ef5fc19
child 6488 271969bb7f95
permissions -rw-r--r--
added translation from IOA to mucalculus and corresponding modelchecker examples;
mueller@6471
     1
(*  Title:      HOL/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
mueller@6471
    12
add_path"~/isabelle/src/HOL/Modelcheck";
mueller@6471
    13
use"~/isabelle/src/HOL/Modelcheck/mucke_oracle.ML";
mueller@6471
    14
use_thy"MuIOAOracle";
mueller@6471
    15
use_thy"Cockpit";
mueller@6471
    16
use_thy"Ring3";
mueller@6471
    17
mueller@6471
    18
reset_path();