diff -r 2756a73f63a5 -r c63e5220ed77 src/HOL/Modelcheck/MuckeExample2.thy
--- a/src/HOL/Modelcheck/MuckeExample2.thy	Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/MuckeExample2.thy	Tue Sep 06 16:24:53 2005 +0200
@@ -4,24 +4,29 @@
     Copyright   1997  TU Muenchen
 *)
 
-
-MuckeExample2 = MuckeSyn +
-
-consts
-
-  Init  :: "bool pred"
-  R	:: "[bool,bool] => bool"
-  Reach	:: "bool pred"
-  Reach2:: "bool pred"
+theory MuckeExample2
+imports MuckeSyn
+begin
 
-defs
-
-  Init_def " Init x == x"
-
-  R_def "R x y == (x & ~y) | (~x & y)"
+constdefs
+  Init  :: "bool pred"
+  "Init x == x"
+  R     :: "[bool,bool] => bool"
+  "R x y == (x & ~y) | (~x & y)"
+  Reach :: "bool pred"
+  "Reach == mu (%Q x. Init x | (? y. Q y & R y x))"
+  Reach2:: "bool pred"
+  "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))"
 
-  Reach_def "Reach == mu (%Q x. Init x | (? y. Q y & R y x))"
+lemmas Reach_rws = Init_def R_def Reach_def Reach2_def
 
-  Reach2_def "Reach2 == mu (%Q x. Reach x | (? y. Q y & R y x))"
+lemma Reach: "Reach2 True"
+  apply (tactic {* simp_tac (Mucke_ss addsimps (thms "Reach_rws")) 1 *})
+  apply (tactic {* mc_mucke_tac [] 1 *})
+  done
 
-end
\ No newline at end of file
+(*alternative:*)
+lemma Reach': "Reach2 True"
+  by (tactic {* mc_mucke_tac (thms "Reach_rws") 1 *})
+
+end