src/HOL/IMP/Transition.thy
changeset 4897 be11be0b6ea1
parent 4757 02b86e36e98f
child 4906 0537ee95d004
     1.1 --- a/src/HOL/IMP/Transition.thy	Tue May 05 17:28:22 1998 +0200
     1.2 +++ b/src/HOL/IMP/Transition.thy	Wed May 06 11:46:00 1998 +0200
     1.3 @@ -24,7 +24,7 @@
     1.4  
     1.5  inductive evalc1
     1.6    intrs
     1.7 -    Assign "(x := a,s) -1-> (SKIP,s[a s / x])"
     1.8 +    Assign "(x := a,s) -1-> (SKIP,s[x := a s])"
     1.9  
    1.10      Semi1   "(SKIP;c,s) -1-> (c,s)"	
    1.11      Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"