# HG changeset patch
# User nipkow
# Date 830801733 -7200
# Node ID a26fbeaaaabd86dc8b5d97eafe33c08fafddb8e2
# Parent  afd3b60660dbf9059ecbf18c47afb99236d78277
Streamlined syntax: -(n)-> is now -n->.

diff -r afd3b60660db -r a26fbeaaaabd src/HOL/IMP/Transition.ML
--- a/src/HOL/IMP/Transition.ML	Mon Apr 29 15:48:27 1996 +0200
+++ b/src/HOL/IMP/Transition.ML	Mon Apr 29 20:15:33 1996 +0200
@@ -16,11 +16,11 @@
 
 val evalc1_cs = relpow_cs addIs (evalc.intrs@evalc1.intrs);
 
-goal Transition.thy "!!c. (c,s) -(0)-> (SKIP,u) ==> c = SKIP & s = u";
+goal Transition.thy "!!c. (c,s) -0-> (SKIP,u) ==> c = SKIP & s = u";
 by(fast_tac evalc1_cs 1);
 val hlemma1 = result();
 
-goal Transition.thy "!!s. (SKIP,s) -(m)-> (SKIP,t) ==> s = t & m = 0";
+goal Transition.thy "!!s. (SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0";
 be rel_pow_E2 1;
 by (Asm_full_simp_tac 1);
 by (eresolve_tac evalc1_elim_cases 1);
@@ -28,7 +28,7 @@
 
 
 goal Transition.thy
-  "!s t u c d. (c,s) -(n)-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
+  "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
 \              (c;d, s) -*-> (SKIP, u)";
 by(nat_ind_tac "n" 1);
  (* case n = 0 *)
@@ -65,8 +65,8 @@
 
 
 goal Transition.thy
-  "!c d s u. (c;d,s) -(n)-> (SKIP,u) --> \
-\            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -(m)-> (SKIP,u) & m <= n)";
+  "!c d s u. (c;d,s) -n-> (SKIP,u) --> \
+\            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)";
 by(nat_ind_tac "n" 1);
  (* case n = 0 *)
  by (fast_tac (HOL_cs addSDs [hlemma1] addss !simpset) 1);
diff -r afd3b60660db -r a26fbeaaaabd src/HOL/IMP/Transition.thy
--- a/src/HOL/IMP/Transition.thy	Mon Apr 29 15:48:27 1996 +0200
+++ b/src/HOL/IMP/Transition.thy	Mon Apr 29 20:15:33 1996 +0200
@@ -12,14 +12,15 @@
 	"@evalc1" :: "[(com*state),(com*state)] => bool"   
 				("_ -1-> _" [81,81] 100)
 	"@evalcn" :: "[(com*state),(com*state)] => nat => bool"
-				("_ -(_)-> _" [81,81] 100)
+				("_ -_-> _" [81,81] 100)
 	"@evalc*" :: "[(com*state),(com*state)] => bool"   
 				("_ -*-> _" [81,81] 100)
 
 translations
+        "x -1-> (y,z)" == "(x,y,z) : evalc1" 
        	"cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
-        "x -(n)-> (y,z)" == "(x,y,z) : evalc1 ^ n" 
-	"cs0 -(n)-> cs1" == "(cs0,cs1) : evalc1 ^ n"
+        "x -n-> (y,z)" == "(x,y,z) : evalc1 ^ n" 
+	"cs0 -n-> cs1" == "(cs0,cs1) : evalc1 ^ n"
 	"x -*-> (y,z)" == "(x,y,z) : evalc1 ^*" 
 	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1 ^*"