src/HOLCF/IOA/Modelcheck/ROOT.ML

 (*  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;
 
 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";