author | wenzelm |
Fri, 08 May 1998 10:15:39 +0200 | |
changeset 4904 | 5f6b2dd1cd11 |
parent 4903 | 0f56199a8d97 |
child 4905 | be73ddff6c5a |
--- a/src/HOLCF/IMP/Denotational.thy Thu May 07 18:34:48 1998 +0200 +++ b/src/HOLCF/IMP/Denotational.thy Fri May 08 10:15:39 1998 +0200 @@ -16,7 +16,7 @@ primrec D com "D(SKIP) = (LAM s. Def(undiscr s))" - "D(X := a) = (LAM s. Def((undiscr s)[a(undiscr s)/X]))" + "D(X := a) = (LAM s. Def((undiscr s)[X := a(undiscr s)]))" "D(c0 ; c1) = (dlift(D c1) oo (D c0))" "D(IF b THEN c1 ELSE c2) = (LAM s. if b(undiscr s) then (D c1)`s else (D c2)`s)"