# HG changeset patch
# User wenzelm
# Date 1126016693 -7200
# Node ID c63e5220ed77bdf6ca743edc8c36044df2037392
# Parent  2756a73f63a5b193fd70b80d056bf9d0f5ef8b73
converted to Isar theory format;

diff -r 2756a73f63a5 -r c63e5220ed77 src/HOL/Modelcheck/CTL.thy
--- a/src/HOL/Modelcheck/CTL.thy	Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/CTL.thy	Tue Sep 06 16:24:53 2005 +0200
@@ -4,18 +4,19 @@
     Copyright   1997  TU Muenchen
 *)
 
-CTL = MuCalculus + 
-
+theory CTL
+imports MuCalculus
+begin
 
 types
   'a trans  = "('a * 'a) set"
 
-consts
-  CEX   ::"['a trans,'a pred, 'a]=>bool"
-  EG    ::"['a trans,'a pred]=> 'a pred"
+constdefs
+  CEX ::"['a trans,'a pred, 'a]=>bool"
+  "CEX N f u == (? v. (f v & (u,v):N))"
+  EG ::"['a trans,'a pred]=> 'a pred"
+  "EG N f == nu (% Q. % u.(f u & CEX N Q u))"
 
-defs
-  CEX_def  "CEX N f u == (? v. (f v & (u,v):N))"
-  EG_def   "EG N f == nu (% Q. % u.(f u & CEX N Q u))"
+ML {* use_legacy_bindings (the_context ()) *}
 
 end
diff -r 2756a73f63a5 -r c63e5220ed77 src/HOL/Modelcheck/EindhovenExample.ML
--- a/src/HOL/Modelcheck/EindhovenExample.ML	Tue Sep 06 08:30:43 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,28 +0,0 @@
-(*  Title:      HOL/Modelcheck/EindhovenExample.ML
-    ID:         $Id$
-    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
-    Copyright   1997  TU Muenchen
-*)
-
-val reach_rws = [reach_def,INIT_def,N_def];
-
-
-Goal "reach (True,True,True)";
-by (simp_tac (Eindhoven_ss addsimps reach_rws) 1);
-
-(*show the current proof state using the model checker syntax*)
-setmp print_mode ["Eindhoven"] pr ();
-
-(* actually invoke the model checker *)
-(* try out after installing the model checker: see the README file *)
-
-(* by (mc_eindhoven_tac 1); *)
-
-(*qed "reach_ex_thm";*)
-
-
-
-(* just to make a proof in this file :-) *)
-Goalw [INIT_def] "INIT (a,b,c) = (~a & ~b &~c)";
-by (Simp_tac 1);
-qed"init_state";
diff -r 2756a73f63a5 -r c63e5220ed77 src/HOL/Modelcheck/EindhovenExample.thy
--- a/src/HOL/Modelcheck/EindhovenExample.thy	Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/EindhovenExample.thy	Tue Sep 06 16:24:53 2005 +0200
@@ -4,28 +4,39 @@
     Copyright   1997  TU Muenchen
 *)
 
-EindhovenExample = CTL + EindhovenSyn + 
-
+theory EindhovenExample
+imports EindhovenSyn CTL
+begin
 
 types
-    state = "bool * bool * bool"
+  state = "bool * bool * bool"
 
-consts
+constdefs
+  INIT :: "state pred"
+  "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
 
-  INIT :: "state pred"
-  N    :: "[state,state] => bool"
+  N :: "[state,state] => bool"
+  "N == % (x1,x2,x3) (y1,y2,y3).
+      (~x1 & ~x2 & ~x3 &   y1 & ~y2 & ~y3) |
+      ( x1 & ~x2 & ~x3 &  ~y1 & ~y2 & ~y3) |
+      ( x1 & ~x2 & ~x3 &   y1 &  y2 &  y3)"
+
   reach:: "state pred"
+  "reach  == mu (%Q x. INIT x | (? y. Q y & N y x))"
 
-defs
-  
-  INIT_def "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd x))"
+lemma init_state: "INIT (a, b, c) = (~a & ~b &~c)"
+  by (simp add: INIT_def)
+
+
+lemmas reach_rws = reach_def INIT_def N_def
 
-   N_def   "N      == % (x1,x2,x3) (y1,y2,y3).
-                        (~x1 & ~x2 & ~x3 &   y1 & ~y2 & ~y3) |   
-	                ( x1 & ~x2 & ~x3 &  ~y1 & ~y2 & ~y3) |   
-	                ( x1 & ~x2 & ~x3 &   y1 &  y2 &  y3)    "
-  
-  reach_def "reach  == mu (%Q x. INIT x | (? y. Q y & N y x))"
-  
+lemma reach_ex: "reach (True, True, True)"
+  apply (tactic {* simp_tac (Eindhoven_ss addsimps (thms "reach_rws")) 1 *})
+  txt {* the current proof state using the model checker syntax: @{subgoals [mode=Eindhoven]} *}
+  pr (Eindhoven)
+  txt {* actually invoke the model checker, try out after installing
+    the model checker: see the README file *}
+  apply (tactic {* mc_eindhoven_tac 1 *})
+  done
 
 end
diff -r 2756a73f63a5 -r c63e5220ed77 src/HOL/Modelcheck/EindhovenSyn.ML
--- a/src/HOL/Modelcheck/EindhovenSyn.ML	Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.ML	Tue Sep 06 16:24:53 2005 +0200
@@ -4,19 +4,11 @@
     Copyright   1997  TU Muenchen
 *)
 
-fun mc_eindhoven_tac i state =
-let val sign = #sign (rep_thm state)
-in 
-case Library.drop(i-1,prems_of state) of
-   [] => Seq.empty |
-   subgoal::_ => 
-	let val concl = Logic.strip_imp_concl subgoal;
-	    val OraAss = invoke_oracle EindhovenSyn.thy "eindhoven_mc" (sign,EindhovenOracleExn concl);
-	in
-	((cut_facts_tac [OraAss] i) THEN (atac i)) state
-        end
-end;
-
+fun mc_eindhoven_tac i state = SUBGOAL (fn (goal, _) =>
+  let
+    val thy = Thm.theory_of_thm state;
+    val assertion = mc_eindhoven_oracle thy (Logic.strip_imp_concl goal);
+  in cut_facts_tac [assertion] i THEN atac i end) i state;
 
 Goalw [split_def] "(f::'a*'b=>'c) = (%(x, y). f (x, y))";
   by (rtac ext 1);
@@ -25,7 +17,7 @@
 qed "pair_eta_expand";
 
 val pair_eta_expand_proc =
-  Simplifier.simproc (Theory.sign_of (the_context ())) "pair_eta_expand" ["f::'a*'b=>'c"]
+  Simplifier.simproc (the_context ()) "pair_eta_expand" ["f::'a*'b=>'c"]
   (fn _ => fn _ => fn t => case t of Abs _ => SOME (mk_meta_eq pair_eta_expand) | _ => NONE);
 
 val Eindhoven_ss =
diff -r 2756a73f63a5 -r c63e5220ed77 src/HOL/Modelcheck/EindhovenSyn.thy
--- a/src/HOL/Modelcheck/EindhovenSyn.thy	Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/EindhovenSyn.thy	Tue Sep 06 16:24:53 2005 +0200
@@ -4,74 +4,59 @@
     Copyright   1997  TU Muenchen
 *)
 
-EindhovenSyn = MuCalculus + 
-  
+theory EindhovenSyn
+imports MuCalculus
+begin
 
 syntax (Eindhoven output)
+  True          :: bool                                 ("TRUE")
+  False         :: bool                                 ("FALSE")
 
-  True		:: bool					("TRUE")
-  False		:: bool					("FALSE")
+  Not           :: "bool => bool"                       ("NOT _" [40] 40)
+  "op &"        :: "[bool, bool] => bool"               (infixr "AND" 35)
+  "op |"        :: "[bool, bool] => bool"               (infixr "OR" 30)
 
-  Not		:: bool => bool				("NOT _" [40] 40)
-  "op &"	:: [bool, bool] => bool			(infixr "AND" 35)
-  "op |"	:: [bool, bool] => bool			(infixr "OR" 30)
+  "ALL "        :: "[idts, bool] => bool"               ("'((3A _./ _)')" [0, 10] 10)
+  "EX "         :: "[idts, bool] => bool"               ("'((3E _./ _)')" [0, 10] 10)
+   "_lambda"    :: "[pttrns, 'a] => 'b"                 ("(3L _./ _)" 10)
+
+  "_idts"       :: "[idt, idts] => idts"                ("_,/_" [1, 0] 0)
+  "_pattern"    :: "[pttrn, patterns] => pttrn"         ("_,/_" [1, 0] 0)
+
+  "Mu "         :: "[idts, 'a pred] => 'a pred"         ("(3[mu _./ _])" 1000)
+  "Nu "         :: "[idts, 'a pred] => 'a pred"         ("(3[nu _./ _])" 1000)
+
+ML {*
+  val trace_eindhoven = ref false;
+*}
 
-  "! " 		:: [idts, bool] => bool			("'((3A _./ _)')" [0, 10] 10)
-  "? "		:: [idts, bool] => bool			("'((3E _./ _)')" [0, 10] 10)
-  "ALL " 	:: [idts, bool] => bool			("'((3A _./ _)')" [0, 10] 10)
-  "EX "		:: [idts, bool] => bool			("'((3E _./ _)')" [0, 10] 10)
-   "_lambda"	:: [pttrns, 'a] => 'b			("(3L _./ _)" 10)
+oracle mc_eindhoven_oracle ("term") =
+{*
+let
+  val eindhoven_term =
+    setmp print_mode ["Eindhoven"] o Sign.string_of_term;
 
-  "_idts"     	:: [idt, idts] => idts		        ("_,/_" [1, 0] 0)
-  "_pattern"    :: [pttrn, patterns] => pttrn     	("_,/_" [1, 0] 0)
-
-  "Mu "		:: [idts, 'a pred] => 'a pred		("(3[mu _./ _])" 1000)
-  "Nu "		:: [idts, 'a pred] => 'a pred		("(3[nu _./ _])" 1000)
-
-oracle
-  eindhoven_mc = mk_eindhoven_mc_oracle
+  fun call_mc s =
+    let
+      val eindhoven_home = getenv "EINDHOVEN_HOME";
+      val pmu =
+        if eindhoven_home = "" then error "Environment variable EINDHOVEN_HOME not set"
+        else eindhoven_home ^ "/pmu";
+    in execute ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w") end;
+in
+  fn thy => fn goal =>
+    let
+      val s = eindhoven_term thy goal;
+      val debug = tracing ("MC debugger: " ^ s);
+      val result = call_mc s;
+    in
+      if ! trace_eindhoven then writeln (cat_lines [s, "----", result]) else ();
+      (case result of
+        "TRUE\n"  => goal |
+        "FALSE\n" => error "MC oracle yields FALSE" |
+      _ => error ("MC syntax error: " ^ result))
+    end
+end
+*}
 
 end
-
-
-
-ML
-
-
-exception EindhovenOracleExn of term;
-
-
-val trace_mc = ref false;
-
-local
-
-fun termtext sign term =
-  setmp print_mode ["Eindhoven"]
-    (Sign.string_of_term sign) term;
-
-fun call_mc s =
-  let
-    val eindhoven_home = getenv "EINDHOVEN_HOME";
-    val pmu =
-      if eindhoven_home = "" then error "Environment variable EINDHOVEN_HOME not set"
-      else eindhoven_home ^ "/pmu";
-  in execute ("echo \"" ^ s ^ "\" | " ^ pmu ^ " -w") end;
-
-in
-
-fun mk_eindhoven_mc_oracle (sign, EindhovenOracleExn trm) =
-  let
-    val tmtext = termtext sign trm;
-    val debug = writeln ("MC debugger: " ^ tmtext);
-    val result = call_mc tmtext;
-  in
-    if ! trace_mc then
-      (writeln tmtext; writeln("----"); writeln result)
-    else ();
-    (case result of
-      "TRUE\n"  =>  trm |
-      "FALSE\n" => (error "MC oracle yields FALSE") |
-    _ => (error ("MC syntax error: " ^ result)))
-  end;
-
-end;
diff -r 2756a73f63a5 -r c63e5220ed77 src/HOL/Modelcheck/MuCalculus.ML
--- a/src/HOL/Modelcheck/MuCalculus.ML	Tue Sep 06 08:30:43 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,38 +0,0 @@
-(*  Title:      HOL/Modelcheck/MuCalculus.ML
-    ID:         $Id$
-    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
-    Copyright   1997  TU Muenchen
-*)
-
-exception MCOracleExn of term;
-exception MCFailureExn of string;
-
-
-val trace_mc = ref false;
-
-local
-
-fun termtext sign term =
-  setmp print_mode ["Eindhoven"] (Sign.string_of_term sign) term;
-
-fun call_mc s =
-  execute ( "echo \"" ^ s ^ "\" | pmu -w" );
-
-in
-
-fun mk_mc_oracle (sign, MCOracleExn trm) =
-  let
-    val tmtext = termtext sign trm;
-    val debug = writeln ("MC debugger: " ^ tmtext);
-    val result = call_mc tmtext;
-  in
-    if ! trace_mc then
-      (writeln tmtext; writeln("----"); writeln result)
-    else ();
-    (case result of
-      "TRUE\n"  =>  trm |
-      "FALSE\n" => (error "MC oracle yields FALSE") |
-    _ => (error ("MC syntax error: " ^ result)))
-  end;
-
-end;
diff -r 2756a73f63a5 -r c63e5220ed77 src/HOL/Modelcheck/MuCalculus.thy
--- a/src/HOL/Modelcheck/MuCalculus.thy	Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/MuCalculus.thy	Tue Sep 06 16:24:53 2005 +0200
@@ -4,23 +4,26 @@
     Copyright   1997  TU Muenchen
 *)
 
-MuCalculus = Main +
+theory MuCalculus
+imports Main
+begin
 
 types
  'a pred = "'a=>bool"
 
-consts
-
+constdefs
   Charfun :: "'a set => 'a pred"
-  mu     :: "('a pred => 'a pred) => 'a pred"  (binder "Mu " 10)
-  nu     :: "('a pred => 'a pred) => 'a pred"  (binder "Nu " 10)
+  "Charfun == (% A.% x. x:A)"
+
   monoP  :: "('a pred => 'a pred) => bool"
+  "monoP f == mono(Collect o f o Charfun)"
 
-defs
+  mu :: "('a pred => 'a pred) => 'a pred"    (binder "Mu " 10)
+  "mu f == Charfun(lfp(Collect o f o Charfun))"
 
-Charfun_def      "Charfun     == (% A.% x. x:A)"
-monoP_def        "monoP f     == mono(Collect o f o Charfun)"
-mu_def           "mu f        == Charfun(lfp(Collect o f o Charfun))"
-nu_def           "nu f        == Charfun(gfp(Collect o f o Charfun))"
+  nu :: "('a pred => 'a pred) => 'a pred"    (binder "Nu " 10)
+  "nu f == Charfun(gfp(Collect o f o Charfun))"
+
+ML {* use_legacy_bindings (the_context ()) *}
 
 end
diff -r 2756a73f63a5 -r c63e5220ed77 src/HOL/Modelcheck/MuckeExample1.ML
--- a/src/HOL/Modelcheck/MuckeExample1.ML	Tue Sep 06 08:30:43 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-(*  Title:      HOL/Modelcheck/MuckeExample1.ML
-    ID:         $Id$
-    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
-    Copyright   1997  TU Muenchen
-*)
-
-val reach_rws = [INIT_def,N_def,reach_def];
-
-Goal "reach (True,True,True)";
-by (simp_tac (Mucke_ss addsimps reach_rws) 1); 
-by (mc_mucke_tac [] 1);
-qed "reach_ex_thm1";
-
-(*alternative*)
-Goal "reach (True,True,True)";
-by (mc_mucke_tac reach_rws 1);
-qed "reach_ex_thm1'";
diff -r 2756a73f63a5 -r c63e5220ed77 src/HOL/Modelcheck/MuckeExample1.thy
--- a/src/HOL/Modelcheck/MuckeExample1.thy	Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/MuckeExample1.thy	Tue Sep 06 16:24:53 2005 +0200
@@ -4,31 +4,34 @@
     Copyright   1997  TU Muenchen
 *)
 
-MuckeExample1 = MuckeSyn + 
-
-
+theory MuckeExample1
+imports MuckeSyn
+begin
 
 types
-    state = "bool * bool * bool"
-
-consts
-
-  INIT :: "state pred"
-  N    :: "[state,state] => bool"
-  reach:: "state pred"
+  state = "bool * bool * bool"
 
-defs
-  
-  INIT_def "INIT x ==  ~(fst x)&~(fst (snd x))&~(snd (snd x))"
+constdefs
+  INIT :: "state pred"
+  "INIT x ==  ~(fst x)&~(fst (snd x))&~(snd (snd x))"
+  N    :: "[state,state] => bool"
+  "N x y == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x));
+                y1 = fst(y); y2 = fst(snd(y)); y3 = snd(snd(y))
+            in (~x1&~x2&~x3 & y1&~y2&~y3) |
+               (x1&~x2&~x3 & ~y1&~y2&~y3) |
+               (x1&~x2&~x3 & y1&y2&y3)"
+  reach:: "state pred"
+  "reach  == mu (%Q x. INIT x | (? y. Q y & N y x))"
 
-  N_def   "N x y == let x1 = fst(x); x2 = fst(snd(x)); x3 = snd(snd(x));   
-	                  y1 = fst(y); y2 = fst(snd(y)); y3 = snd(snd(y)) 
-                     in (~x1&~x2&~x3 & y1&~y2&~y3) |   
-	                (x1&~x2&~x3 & ~y1&~y2&~y3) |   
-	                (x1&~x2&~x3 & y1&y2&y3)    "
-  
-  reach_def "reach  == mu (%Q x. INIT x | (? y. Q y & N y x))"
-  
+lemmas reach_rws = INIT_def N_def reach_def
+
+lemma reach_ex1: "reach (True,True,True)"
+  apply (tactic {* simp_tac (Mucke_ss addsimps (thms "reach_rws")) 1 *})
+  apply (tactic {* mc_mucke_tac [] 1 *})
+  done
+
+(*alternative*)
+lemma reach_ex' "reach (True,True,True)"
+  by (tactic {* mc_mucke_tac (thms "reach_rws") 1 *})
 
 end
-
diff -r 2756a73f63a5 -r c63e5220ed77 src/HOL/Modelcheck/MuckeExample2.ML
--- a/src/HOL/Modelcheck/MuckeExample2.ML	Tue Sep 06 08:30:43 2005 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-(*  Title:      HOL/Modelcheck/MuckeExample2.ML
-    ID:         $Id$
-    Author:     Olaf Mueller, Jan Philipps, Robert Sandner
-    Copyright   1997  TU Muenchen
-*)
-
-
-(* prints the mucke output on the screen *)
-(* trace_mc := true; *)
-val Reach_rws = [Init_def,R_def,Reach_def,Reach2_def];
-
-Goal "Reach2 True";
-by (simp_tac (Mucke_ss addsimps Reach_rws) 1);
-by (mc_mucke_tac [] 1);
-qed "Reach_thm";
-
-(*alternative:*)
-goal thy "Reach2 True";
-by (mc_mucke_tac Reach_rws 1);
-qed "Reach_thm'";
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
diff -r 2756a73f63a5 -r c63e5220ed77 src/HOL/Modelcheck/MuckeSyn.ML
--- a/src/HOL/Modelcheck/MuckeSyn.ML	Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.ML	Tue Sep 06 16:24:53 2005 +0200
@@ -49,7 +49,7 @@
 
 local
 
-  val move_thm = prove_goal MuckeSyn.thy "[| a = b ==> P a; a = b |] ==> P b"
+  val move_thm = prove_goal (the_context ()) "[| a = b ==> P a; a = b |] ==> P b"
 	(fn prems => [cut_facts_tac prems 1, dtac sym 1, hyp_subst_tac 1,
 		     REPEAT (resolve_tac prems 1)]);
 
@@ -86,9 +86,9 @@
 (* Type of call_mucke_tac has changed: an argument t of type thy was inserted (TH); *)
 (* Normally t can be user-instantiated by the value thy of the Isabelle context     *)
 fun call_mucke_tac i state =
-let val sign = #sign (rep_thm state);
+let val thy = Thm.theory_of_thm state;
     val (subgoal::_) = Library.drop(i-1,prems_of state);
-    val OraAss = invoke_oracle MuckeSyn.thy "Mucke" (sign,MuckeOracleExn (subgoal));
+    val OraAss = mc_mucke_oracle thy subgoal;
 in 
 (cut_facts_tac [OraAss] i) state
 end;
diff -r 2756a73f63a5 -r c63e5220ed77 src/HOL/Modelcheck/MuckeSyn.thy
--- a/src/HOL/Modelcheck/MuckeSyn.thy	Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/MuckeSyn.thy	Tue Sep 06 16:24:53 2005 +0200
@@ -4,76 +4,73 @@
     Copyright   1999  TU Muenchen
 *)
 
+theory MuckeSyn
+imports MuCalculus
+uses "mucke_oracle.ML"
+begin
 
-MuckeSyn = MuCalculus + 
-
-(* extended with some operators and case treatment (which requires postprocessing with 
+(* extended with some operators and case treatment (which requires postprocessing with
 transform_case (from MuCalculus) (TH) *)
 
-types
-  mutype 
+nonterminals
+  mutype
   decl decls
-  cases_syn case_syn 
+  cases_syn case_syn
 
 syntax (Mucke output)
-  True		:: bool					("true")
-  False		:: bool					("false")
-  Not		:: bool => bool				("! _" [40] 40)
-  If		:: [bool, 'a, 'a] => 'a		("('(if'((_)')/ '((_)')/ else/ '((_)'))')" 10)
-  
-  "op &"	:: [bool, bool] => bool			(infixr "&" 35)
-  "op |"	:: [bool, bool] => bool			(infixr "|" 30)
-  "op -->"	:: [bool, bool] => bool			(infixr "->" 25)
-  "op ="        :: ['a, 'a] => bool                 ("(_ =/ _)" [51, 51] 50)
-  "_not_equal"  :: ['a, 'a] => bool                 ("(_ !=/ _)" [51, 51] 50)
+  True          :: bool                                 ("true")
+  False         :: bool                                 ("false")
+  Not           :: "bool => bool"                       ("! _" [40] 40)
+  If            :: "[bool, 'a, 'a] => 'a"       ("('(if'((_)')/ '((_)')/ else/ '((_)'))')" 10)
 
-  "! " 		:: [idts, bool] => bool			("'((3forall _./ _)')" [0, 10] 10)
-  "? "		:: [idts, bool] => bool			("'((3exists _./ _)')" [0, 10] 10)
-  "ALL "        :: [idts, bool] => bool                 ("'((3forall _./ _)')" [0, 10] 10)
-  "EX "         :: [idts, bool] => bool                 ("'((3exists _./ _)')" [0, 10] 10)
+  "op &"        :: "[bool, bool] => bool"               (infixr "&" 35)
+  "op |"        :: "[bool, bool] => bool"               (infixr "|" 30)
+  "op -->"      :: "[bool, bool] => bool"               (infixr "->" 25)
+  "op ="        :: "['a, 'a] => bool"                   ("(_ =/ _)" [51, 51] 50)
+  "_not_equal"  :: "['a, 'a] => bool"                   ("(_ !=/ _)" [51, 51] 50)
 
-  "_lambda"	:: [idts, 'a] => 'b  			("(3L _./ _)" 10)
-  "_applC"	:: [('b => 'a), cargs] => aprop		("(1_/ '(_'))" [1000,1000] 999)
-  "_cargs" 	:: ['a, cargs] => cargs         	("_,/ _" [1000,1000] 1000)
+  "ALL "        :: "[idts, bool] => bool"               ("'((3forall _./ _)')" [0, 10] 10)
+  "EX "         :: "[idts, bool] => bool"               ("'((3exists _./ _)')" [0, 10] 10)
 
-  "_idts"     	:: [idt, idts] => idts		        ("_,/ _" [1, 0] 0)
+  "_lambda"     :: "[idts, 'a] => 'b"                   ("(3L _./ _)" 10)
+  "_applC"      :: "[('b => 'a), cargs] => aprop"       ("(1_/ '(_'))" [1000,1000] 999)
+  "_cargs"      :: "['a, cargs] => cargs"               ("_,/ _" [1000,1000] 1000)
+
+  "_idts"       :: "[idt, idts] => idts"                ("_,/ _" [1, 0] 0)
 
   "_tuple"      :: "'a => tuple_args => 'a * 'b"        ("(1_,/ _)")
-(* "@pttrn"     :: [pttrn, pttrns] => pttrn     	("_,/ _" [1, 0] 0) 
-  "_pattern"    :: [pttrn, patterns] => pttrn           ("_,/ _" [1, 0] 0) *)
-
+(* "@pttrn"     :: "[pttrn, pttrns] => pttrn"           ("_,/ _" [1, 0] 0)
+  "_pattern"    :: "[pttrn, patterns] => pttrn"         ("_,/ _" [1, 0] 0) *)
 
-  "_decl"	:: [mutype,pttrn] => decl		("_ _")
-  "_decls"	:: [decl,decls] => decls		("_,/ _")
-  ""		:: decl => decls			("_")
-  "_mu"		:: [decl,decls,'a pred] => 'a pred	("mu _ '(_') _ ;")
-  "_mudec"	:: [decl,decls] => 'a pred		("mu _ '(_') ;") 
-  "_nu"		:: [decl,decls,'a pred] => 'a pred	("nu _ '(_') _ ;") 
-  "_nudec"	:: [decl,decls] => 'a pred		("nu _ '(_') ;") 
-  "_fun"  	:: [decl,decls,'a pred] => 'a pred 	("_ '(_') _ ;")
-  "_dec"	:: [decl,decls] => 'a pred		("_ '(_') ;")
+  "_decl"       :: "[mutype,pttrn] => decl"             ("_ _")
+  "_decls"      :: "[decl,decls] => decls"              ("_,/ _")
+  ""            :: "decl => decls"                      ("_")
+  "_mu"         :: "[decl,decls,'a pred] => 'a pred"    ("mu _ '(_') _ ;")
+  "_mudec"      :: "[decl,decls] => 'a pred"            ("mu _ '(_') ;")
+  "_nu"         :: "[decl,decls,'a pred] => 'a pred"    ("nu _ '(_') _ ;")
+  "_nudec"      :: "[decl,decls] => 'a pred"            ("nu _ '(_') ;")
+  "_fun"        :: "[decl,decls,'a pred] => 'a pred"    ("_ '(_') _ ;")
+  "_dec"        :: "[decl,decls] => 'a pred"            ("_ '(_') ;")
+
+  "_Ex"         :: "[decl,idts,'a pred] => 'a pred"     ("'((3exists _ _./ _)')")
+  "_All"        :: "[decl,idts,'a pred] => 'a pred"     ("'((3forall _ _./ _)')")
 
-  "_Ex"  	:: [decl,idts,'a pred] => 'a pred	("'((3exists _ _./ _)')")
-  "_All"	:: [decl,idts,'a pred] => 'a pred	("'((3forall _ _./ _)')")
+  "Mu "         :: "[idts, 'a pred] => 'a pred"         ("(3mu _./ _)" 1000)
+  "Nu "         :: "[idts, 'a pred] => 'a pred"         ("(3nu _./ _)" 1000)
+
+  "_case_syntax":: "['a, cases_syn] => 'b"              ("(case*_* / _ / esac*)" 10)
+  "_case1"      :: "['a, 'b] => case_syn"               ("(2*= _ :/ _;)" 10)
+  ""            :: "case_syn => cases_syn"              ("_")
+  "_case2"      :: "[case_syn, cases_syn] => cases_syn" ("_/ _")
 
-  "Mu "		:: [idts, 'a pred] => 'a pred		("(3mu _./ _)" 1000)
-  "Nu "		:: [idts, 'a pred] => 'a pred		("(3nu _./ _)" 1000)
-  
-  "_case_syntax":: ['a, cases_syn] => 'b            ("(case*_* / _ / esac*)" 10)
-  "_case1"      :: ['a, 'b] => case_syn             ("(2*= _ :/ _;)" 10)
-  ""            :: case_syn => cases_syn            ("_")
-  "_case2"      :: [case_syn, cases_syn] => cases_syn   ("_/ _")
-(* Terms containing a case statement must be post-processed with the function  *)
-(* transform_case, defined in MuCalculus.ML. There, all asterikses before the  *)
-(* "=" will be replaced by the expression between the two asterikses following *)
-(* "case" and the asteriks after esac will be deleted                          *)
+(*Terms containing a case statement must be post-processed with the
+  ML function transform_case. There, all asterikses before the "="
+  will be replaced by the expression between the two asterisks
+  following "case" and the asterisk after esac will be deleted *)
 
-oracle
-  Mucke = mk_mucke_mc_oracle
+oracle mc_mucke_oracle ("term") =
+  mk_mc_mucke_oracle
 
 end
 
 
-
-  
-
diff -r 2756a73f63a5 -r c63e5220ed77 src/HOL/Modelcheck/ROOT.ML
--- a/src/HOL/Modelcheck/ROOT.ML	Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/ROOT.ML	Tue Sep 06 16:24:53 2005 +0200
@@ -5,6 +5,14 @@
 Basic Modelchecker examples.
 *)
 
+time_use_thy "CTL";
+
+
+(* Einhoven model checker *)
+
+time_use_thy "EindhovenSyn";
+if_eindhoven_enabled time_use_thy "EindhovenExample";
+
 
 (* Mucke -- mu-calculus model checker from Karlsruhe *)
 
@@ -15,9 +23,3 @@
 if_mucke_enabled time_use_thy "MuckeExample2";
 
 
-(* Einhoven model checker *)
-
-time_use_thy "CTL";
-time_use_thy "EindhovenSyn";
-
-if_eindhoven_enabled time_use_thy "EindhovenExample";
diff -r 2756a73f63a5 -r c63e5220ed77 src/HOL/Modelcheck/mucke_oracle.ML
--- a/src/HOL/Modelcheck/mucke_oracle.ML	Tue Sep 06 08:30:43 2005 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML	Tue Sep 06 16:24:53 2005 +0200
@@ -1,8 +1,6 @@
 
 (* $Id$ *)
 
-exception MuckeOracleExn of term;
-
 val trace_mc = ref false; 
 
 
@@ -1017,9 +1015,8 @@
 end;
 
 (**********************************************************)
-(* mk_mc_oracle:  new argument of MuckeOracleExn: source_thy *)
 
-fun mk_mucke_mc_oracle (sign, MuckeOracleExn (subgoal)) = 
+fun mk_mc_mucke_oracle sign subgoal = 
   let 	val Freesubgoal = freeze_thaw subgoal;
 
 	val prems = Logic.strip_imp_prems Freesubgoal;