--- a/src/HOLCF/IOA/Modelcheck/ROOT.ML Thu Aug 19 21:31:36 1999 +0200
+++ b/src/HOLCF/IOA/Modelcheck/ROOT.ML Thu Aug 19 21:49:10 1999 +0200
@@ -1,10 +1,8 @@
(* Title: HOLCF/IOA/Modelcheck/ROOT.ML
ID: $Id$
- Author: Olaf Mueller
- Copyright 1997 TU Muenchen
+ Author: Olaf Mueller and Tobias Hamberger, TU Muenchen
-This is the ROOT file for the formalization of a semantic model of
-I/O-Automata. See the README.html file for details.
+Modelchecker setup for I/O automata.
*)
goals_limit := 1;
@@ -12,5 +10,7 @@
use "../../../HOL/Modelcheck/mucke_oracle.ML";
use_thy "../../../HOL/Modelcheck/MuckeSyn";
use_thy "MuIOAOracle";
-use_thy "Cockpit";
-use_thy "Ring3";
+
+(*examples*)
+if_mucke_enabled use_thy "Cockpit";
+if_mucke_enabled use_thy "Ring3";