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)"