Streamlined syntax: -(n)-> is now -n->.
authornipkow
Mon Apr 29 20:15:33 1996 +0200 (1996-04-29)
changeset 1701a26fbeaaaabd
parent 1700 afd3b60660db
child 1702 4aa538e82f76
Streamlined syntax: -(n)-> is now -n->.
src/HOL/IMP/Transition.ML
src/HOL/IMP/Transition.thy
     1.1 --- a/src/HOL/IMP/Transition.ML	Mon Apr 29 15:48:27 1996 +0200
     1.2 +++ b/src/HOL/IMP/Transition.ML	Mon Apr 29 20:15:33 1996 +0200
     1.3 @@ -16,11 +16,11 @@
     1.4  
     1.5  val evalc1_cs = relpow_cs addIs (evalc.intrs@evalc1.intrs);
     1.6  
     1.7 -goal Transition.thy "!!c. (c,s) -(0)-> (SKIP,u) ==> c = SKIP & s = u";
     1.8 +goal Transition.thy "!!c. (c,s) -0-> (SKIP,u) ==> c = SKIP & s = u";
     1.9  by(fast_tac evalc1_cs 1);
    1.10  val hlemma1 = result();
    1.11  
    1.12 -goal Transition.thy "!!s. (SKIP,s) -(m)-> (SKIP,t) ==> s = t & m = 0";
    1.13 +goal Transition.thy "!!s. (SKIP,s) -m-> (SKIP,t) ==> s = t & m = 0";
    1.14  be rel_pow_E2 1;
    1.15  by (Asm_full_simp_tac 1);
    1.16  by (eresolve_tac evalc1_elim_cases 1);
    1.17 @@ -28,7 +28,7 @@
    1.18  
    1.19  
    1.20  goal Transition.thy
    1.21 -  "!s t u c d. (c,s) -(n)-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
    1.22 +  "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
    1.23  \              (c;d, s) -*-> (SKIP, u)";
    1.24  by(nat_ind_tac "n" 1);
    1.25   (* case n = 0 *)
    1.26 @@ -65,8 +65,8 @@
    1.27  
    1.28  
    1.29  goal Transition.thy
    1.30 -  "!c d s u. (c;d,s) -(n)-> (SKIP,u) --> \
    1.31 -\            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -(m)-> (SKIP,u) & m <= n)";
    1.32 +  "!c d s u. (c;d,s) -n-> (SKIP,u) --> \
    1.33 +\            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)";
    1.34  by(nat_ind_tac "n" 1);
    1.35   (* case n = 0 *)
    1.36   by (fast_tac (HOL_cs addSDs [hlemma1] addss !simpset) 1);
     2.1 --- a/src/HOL/IMP/Transition.thy	Mon Apr 29 15:48:27 1996 +0200
     2.2 +++ b/src/HOL/IMP/Transition.thy	Mon Apr 29 20:15:33 1996 +0200
     2.3 @@ -12,14 +12,15 @@
     2.4  	"@evalc1" :: "[(com*state),(com*state)] => bool"   
     2.5  				("_ -1-> _" [81,81] 100)
     2.6  	"@evalcn" :: "[(com*state),(com*state)] => nat => bool"
     2.7 -				("_ -(_)-> _" [81,81] 100)
     2.8 +				("_ -_-> _" [81,81] 100)
     2.9  	"@evalc*" :: "[(com*state),(com*state)] => bool"   
    2.10  				("_ -*-> _" [81,81] 100)
    2.11  
    2.12  translations
    2.13 +        "x -1-> (y,z)" == "(x,y,z) : evalc1" 
    2.14         	"cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
    2.15 -        "x -(n)-> (y,z)" == "(x,y,z) : evalc1 ^ n" 
    2.16 -	"cs0 -(n)-> cs1" == "(cs0,cs1) : evalc1 ^ n"
    2.17 +        "x -n-> (y,z)" == "(x,y,z) : evalc1 ^ n" 
    2.18 +	"cs0 -n-> cs1" == "(cs0,cs1) : evalc1 ^ n"
    2.19  	"x -*-> (y,z)" == "(x,y,z) : evalc1 ^*" 
    2.20  	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1 ^*"
    2.21