changeset 9241 | f961c1fdff50 |
parent 5608 | a82a038a3e7a |
child 12431 | 07ec657249e5 |
--- a/src/HOL/IMP/Denotation.thy Tue Jul 04 10:54:32 2000 +0200 +++ b/src/HOL/IMP/Denotation.thy Tue Jul 04 10:54:46 2000 +0200 @@ -20,7 +20,7 @@ primrec C_skip "C(SKIP) = Id" - C_assign "C(x := a) = {(s,t). t = s[x:=a(s)]}" + C_assign "C(x :== a) = {(s,t). t = s[x::=a(s)]}" C_comp "C(c0 ; c1) = C(c1) O C(c0)" C_if "C(IF b THEN c1 ELSE c2) = {(s,t). (s,t) : C(c1) & b(s)} Un {(s,t). (s,t) : C(c2) & ~ b(s)}"