# HG changeset patch
# User mueller
# Date 864116899 -7200
# Node ID cee363fc07d796de7755fd12fd72fb6a94693a63
# Parent  4ea2aa9f93a51dba89332ff3ab0e9c70a0f771d1
little changes

diff -r 4ea2aa9f93a5 -r cee363fc07d7 src/HOL/Modelcheck/Example.ML
--- a/src/HOL/Modelcheck/Example.ML	Mon May 19 15:22:41 1997 +0200
+++ b/src/HOL/Modelcheck/Example.ML	Tue May 20 10:28:19 1997 +0200
@@ -13,8 +13,10 @@
 (*show the current proof state using the model checker syntax*)
 setmp print_mode ["Eindhoven"] pr ();
 
-(*actually invoke the model checker*)
-by (mc_tac 1);
+(* actually invoke the model checker *)
+(* try out after installing the model checker: see the README file *)
+
+(* by (mc_tac 1); *)
 
 (*qed "reach_ex_thm1";*)
 
diff -r 4ea2aa9f93a5 -r cee363fc07d7 src/HOL/Modelcheck/Example.thy
--- a/src/HOL/Modelcheck/Example.thy	Mon May 19 15:22:41 1997 +0200
+++ b/src/HOL/Modelcheck/Example.thy	Tue May 20 10:28:19 1997 +0200
@@ -20,11 +20,10 @@
   
   INIT_def "INIT x == ~(fst x)&~(fst (snd x))&~(snd (snd 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)    "
+   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))"