# HG changeset patch
# User wenzelm
# Date 894635101 -7200
# Node ID 0537ee95d00402d2f1d394d8840d965f7d698df7
# Parent  be73ddff6c5a357e9b0ed8f138d5b4584ed03324
fixed translations;

diff -r be73ddff6c5a -r 0537ee95d004 src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Fri May 08 13:54:45 1998 +0200
+++ b/src/HOL/IMP/Transition.thy	Fri May 08 15:45:01 1998 +0200
@@ -8,25 +8,32 @@
 
 Transition = Natural + RelPow +
 
-consts  evalc1    :: "((com*state)*(com*state))set"        
-	"@evalc1" :: "[(com*state),(com*state)] => bool"   
-				("_ -1-> _" [81,81] 100)
-	"@evalcn" :: "[(com*state),(com*state)] => nat => bool"
-				("_ -_-> _" [81,81] 100)
-	"@evalc*" :: "[(com*state),(com*state)] => bool"   
-				("_ -*-> _" [81,81] 100)
+consts  evalc1    :: "((com*state)*(com*state))set"
+
+syntax
+        "@evalc1" :: "[(com*state),(com*state)] => bool"
+                                ("_ -1-> _" [81,81] 100)
+        "@evalcn" :: "[(com*state),(com*state)] => nat => bool"
+                                ("_ -_-> _" [81,81] 100)
+        "@evalc*" :: "[(com*state),(com*state)] => bool"
+                                ("_ -*-> _" [81,81] 100)
 
 translations
-       	"cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
-	"cs0 -n-> cs1" == "(cs0,cs1) : evalc1^n"
-	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1^*"
+  "cs0 -1-> cs1"	== "(cs0,cs1) : evalc1"
+  "cs0 -1-> (c1,s1)"	<= "cs0 -1-> (_args c1 s1)"
+
+  "cs0 -n-> cs1" 	== "(cs0,cs1) : evalc1^n"
+  "cs0 -n-> (c1,s1)" 	<= "cs0 -n-> (_args c1 s1)"
+
+  "cs0 -*-> cs1" 	== "(cs0,cs1) : evalc1^*"
+  "cs0 -*-> (c1,s1)" 	<= "cs0 -*-> (_args c1 s1)"
 
 
 inductive evalc1
   intrs
     Assign "(x := a,s) -1-> (SKIP,s[x := a s])"
 
-    Semi1   "(SKIP;c,s) -1-> (c,s)"	
+    Semi1   "(SKIP;c,s) -1-> (c,s)"     
     Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
 
     IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"