src/HOL/IMP/Transition.thy
changeset 9241 f961c1fdff50
parent 8029 05446a898852
child 9364 e783491b9a1f
     1.1 --- a/src/HOL/IMP/Transition.thy	Tue Jul 04 10:54:32 2000 +0200
     1.2 +++ b/src/HOL/IMP/Transition.thy	Tue Jul 04 10:54:46 2000 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  
     1.5  inductive evalc1
     1.6    intrs
     1.7 -    Assign "(x := a,s) -1-> (SKIP,s[x := a s])"
     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)"