| changeset 9247 | ad9f986616de |
| parent 5192 | 704dd3a6d47d |
| child 10835 | f4745d77e620 |
--- a/src/HOLCF/IMP/Denotational.thy Wed Jul 05 10:28:29 2000 +0200 +++ b/src/HOLCF/IMP/Denotational.thy Wed Jul 05 14:26:58 2000 +0200 @@ -16,7 +16,7 @@ primrec "D(SKIP) = (LAM s. Def(undiscr s))" - "D(X := a) = (LAM s. Def((undiscr s)[X := a(undiscr s)]))" + "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)"