fixed translations;
authorwenzelm
Fri May 08 15:45:01 1998 +0200 (1998-05-08)
changeset 49060537ee95d004
parent 4905 be73ddff6c5a
child 4907 0eb6730de30f
fixed translations;
src/HOL/IMP/Transition.thy
     1.1 --- a/src/HOL/IMP/Transition.thy	Fri May 08 13:54:45 1998 +0200
     1.2 +++ b/src/HOL/IMP/Transition.thy	Fri May 08 15:45:01 1998 +0200
     1.3 @@ -8,25 +8,32 @@
     1.4  
     1.5  Transition = Natural + RelPow +
     1.6  
     1.7 -consts  evalc1    :: "((com*state)*(com*state))set"        
     1.8 -	"@evalc1" :: "[(com*state),(com*state)] => bool"   
     1.9 -				("_ -1-> _" [81,81] 100)
    1.10 -	"@evalcn" :: "[(com*state),(com*state)] => nat => bool"
    1.11 -				("_ -_-> _" [81,81] 100)
    1.12 -	"@evalc*" :: "[(com*state),(com*state)] => bool"   
    1.13 -				("_ -*-> _" [81,81] 100)
    1.14 +consts  evalc1    :: "((com*state)*(com*state))set"
    1.15 +
    1.16 +syntax
    1.17 +        "@evalc1" :: "[(com*state),(com*state)] => bool"
    1.18 +                                ("_ -1-> _" [81,81] 100)
    1.19 +        "@evalcn" :: "[(com*state),(com*state)] => nat => bool"
    1.20 +                                ("_ -_-> _" [81,81] 100)
    1.21 +        "@evalc*" :: "[(com*state),(com*state)] => bool"
    1.22 +                                ("_ -*-> _" [81,81] 100)
    1.23  
    1.24  translations
    1.25 -       	"cs0 -1-> cs1" == "(cs0,cs1) : evalc1"
    1.26 -	"cs0 -n-> cs1" == "(cs0,cs1) : evalc1^n"
    1.27 -	"cs0 -*-> cs1" == "(cs0,cs1) : evalc1^*"
    1.28 +  "cs0 -1-> cs1"	== "(cs0,cs1) : evalc1"
    1.29 +  "cs0 -1-> (c1,s1)"	<= "cs0 -1-> (_args c1 s1)"
    1.30 +
    1.31 +  "cs0 -n-> cs1" 	== "(cs0,cs1) : evalc1^n"
    1.32 +  "cs0 -n-> (c1,s1)" 	<= "cs0 -n-> (_args c1 s1)"
    1.33 +
    1.34 +  "cs0 -*-> cs1" 	== "(cs0,cs1) : evalc1^*"
    1.35 +  "cs0 -*-> (c1,s1)" 	<= "cs0 -*-> (_args c1 s1)"
    1.36  
    1.37  
    1.38  inductive evalc1
    1.39    intrs
    1.40      Assign "(x := a,s) -1-> (SKIP,s[x := a s])"
    1.41  
    1.42 -    Semi1   "(SKIP;c,s) -1-> (c,s)"	
    1.43 +    Semi1   "(SKIP;c,s) -1-> (c,s)"     
    1.44      Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"
    1.45  
    1.46      IfTrue "b s ==> (IF b THEN c1 ELSE c2,s) -1-> (c1,s)"