src/HOL/IMP/Transition.thy
changeset 9241 f961c1fdff50
parent 8029 05446a898852
child 9364 e783491b9a1f
--- a/src/HOL/IMP/Transition.thy	Tue Jul 04 10:54:32 2000 +0200
+++ b/src/HOL/IMP/Transition.thy	Tue Jul 04 10:54:46 2000 +0200
@@ -31,7 +31,7 @@
 
 inductive evalc1
   intrs
-    Assign "(x := a,s) -1-> (SKIP,s[x := a s])"
+    Assign "(x :== a,s) -1-> (SKIP,s[x ::= a s])"
 
     Semi1   "(SKIP;c,s) -1-> (c,s)"     
     Semi2   "(c0,s) -1-> (c2,s1) ==> (c0;c1,s) -1-> (c2;c1,s1)"