diff -r 5a50de9141b5 -r fe09a0c5cebe src/HOL/Modelcheck/ROOT.ML
--- a/src/HOL/Modelcheck/ROOT.ML	Thu Aug 19 19:01:57 1999 +0200
+++ b/src/HOL/Modelcheck/ROOT.ML	Thu Aug 19 19:55:13 1999 +0200
@@ -1,13 +1,23 @@
 (*  Title:      HOL/Modelcheck/ROOT.ML
     ID:         $Id$
-    Author:     Olaf Mueller, Tobias Hamberger, Robert Sandner
-    Copyright   1997  TU Muenchen
+    Author:     Olaf Mueller and Tobias Hamberger and Robert Sandner, TU Muenchen
 
-This is the ROOT file for the Modelchecker examples
+Basic Modelchecker examples.
 *)
 
-use_thy"EindhovenExample";
+
+(* Mucke -- mu-calculus model checker from Karlsruhe *)
+
+use "mucke_oracle.ML";
+use_thy "MuckeSyn";
 
-use"mucke_oracle.ML";
-use_thy"MuckeExample1";
-use_thy"MuckeExample2";
+if_mucke_enabled use_thy "MuckeExample1";
+if_mucke_enabled use_thy "MuckeExample2";
+
+
+(* Einhoven model checker *)
+
+use_thy "CTL";
+use_thy "EindhovenSyn";
+
+if_eindhoven_enabled use_thy "EindhovenExample";