src/HOL/Induct/Com.thy

--- a/src/HOL/Induct/Com.thy	Fri Nov 21 11:54:23 1997 +0100
+++ b/src/HOL/Induct/Com.thy	Fri Nov 21 11:57:58 1997 +0100
@@ -34,6 +34,12 @@
 
 translations  "csig -[eval]-> s" == "(csig,s) : exec eval"
 
+syntax  eval'   :: "[exp*state,nat*state] => 
+		    ((exp*state) * (nat*state)) set => bool"
+						   ("_/ -|[_]-> _" [50,0,50] 50)
+translations
+    "esig -|[eval]-> ns" => "(esig,ns) : eval"
+
 constdefs assign :: [state,nat,loc] => state    ("_[_'/_]" [95,0,0] 95)
   "s[m/x] ==  (%y. if y=x then m else s y)"
 
@@ -43,20 +49,20 @@
   intrs
     Skip    "(SKIP,s) -[eval]-> s"
 
-    Assign  "((e,s), (v,s')) : eval ==> (x := e, s) -[eval]-> s'[v/x]"
+    Assign  "(e,s) -|[eval]-> (v,s') ==> (x := e, s) -[eval]-> s'[v/x]"
 
     Semi    "[| (c0,s) -[eval]-> s2; (c1,s2) -[eval]-> s1 |] 
             ==> (c0 ;; c1, s) -[eval]-> s1"
 
-    IfTrue "[| ((e,s), (0,s')) : eval;  (c0,s') -[eval]-> s1 |] 
+    IfTrue "[| (e,s) -|[eval]-> (0,s');  (c0,s') -[eval]-> s1 |] 
             ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
 
-    IfFalse "[| ((e,s), (1,s')) : eval;  (c1,s') -[eval]-> s1 |] 
+    IfFalse "[| (e,s) -|[eval]->  (1,s');  (c1,s') -[eval]-> s1 |] 
              ==> (IF e THEN c0 ELSE c1, s) -[eval]-> s1"
 
-    WhileFalse "((e,s), (1,s1)) : eval ==> (WHILE e DO c, s) -[eval]-> s1"
+    WhileFalse "(e,s) -|[eval]-> (1,s1) ==> (WHILE e DO c, s) -[eval]-> s1"
 
-    WhileTrue  "[| ((e,s), (0,s1)) : eval;
+    WhileTrue  "[| (e,s) -|[eval]-> (0,s1);
                 (c,s1) -[eval]-> s2;  (WHILE e DO c, s2) -[eval]-> s3 |] 
                 ==> (WHILE e DO c, s) -[eval]-> s3"