src/HOL/IMP/Transition.thy
changeset 4757 02b86e36e98f
parent 1789 aade046ec6d5
child 4897 be11be0b6ea1
     1.1 --- a/src/HOL/IMP/Transition.thy	Tue Mar 24 16:57:40 1998 +0100
     1.2 +++ b/src/HOL/IMP/Transition.thy	Mon Mar 30 21:03:14 1998 +0200
     1.3 @@ -17,12 +17,9 @@
     1.4  				("_ -*-> _" [81,81] 100)
     1.5  
     1.6  translations
     1.7 -        "x -1-> (y,z)" == "(x,y,z) : evalc1" 
     1.8         	"cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
     1.9 -        "x -n-> (y,z)" == "(x,y,z) : evalc1 ^ n" 
    1.10 -	"cs0 -n-> cs1" == "(cs0,cs1) : evalc1 ^ n"
    1.11 -	"x -*-> (y,z)" == "(x,y,z) : evalc1 ^*" 
    1.12 -	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1 ^*"
    1.13 +	"cs0 -n-> cs1" == "(cs0,cs1) : evalc1^n"
    1.14 +	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1^*"
    1.15  
    1.16  
    1.17  inductive evalc1