src/HOL/IMP/Transition.thy
changeset 1701 a26fbeaaaabd
parent 1700 afd3b60660db
child 1789 aade046ec6d5
     1.1 --- a/src/HOL/IMP/Transition.thy	Mon Apr 29 15:48:27 1996 +0200
     1.2 +++ b/src/HOL/IMP/Transition.thy	Mon Apr 29 20:15:33 1996 +0200
     1.3 @@ -12,14 +12,15 @@
     1.4  	"@evalc1" :: "[(com*state),(com*state)] => bool"   
     1.5  				("_ -1-> _" [81,81] 100)
     1.6  	"@evalcn" :: "[(com*state),(com*state)] => nat => bool"
     1.7 -				("_ -(_)-> _" [81,81] 100)
     1.8 +				("_ -_-> _" [81,81] 100)
     1.9  	"@evalc*" :: "[(com*state),(com*state)] => bool"   
    1.10  				("_ -*-> _" [81,81] 100)
    1.11  
    1.12  translations
    1.13 +        "x -1-> (y,z)" == "(x,y,z) : evalc1" 
    1.14         	"cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
    1.15 -        "x -(n)-> (y,z)" == "(x,y,z) : evalc1 ^ n" 
    1.16 -	"cs0 -(n)-> cs1" == "(cs0,cs1) : evalc1 ^ n"
    1.17 +        "x -n-> (y,z)" == "(x,y,z) : evalc1 ^ n" 
    1.18 +	"cs0 -n-> cs1" == "(cs0,cs1) : evalc1 ^ n"
    1.19  	"x -*-> (y,z)" == "(x,y,z) : evalc1 ^*" 
    1.20  	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1 ^*"
    1.21