# HG changeset patch # User wenzelm # Date 1368781559 -7200 # Node ID 0476162187c484920f4dc2adca01efc12016689e # Parent bc01725d79182d7940057dd5863d6ce66d6bb268 repair after bc01725d7918; diff -r bc01725d7918 -r 0476162187c4 src/HOL/HOLCF/IMP/Denotational.thy --- a/src/HOL/HOLCF/IMP/Denotational.thy Fri May 17 08:19:52 2013 +0200 +++ b/src/HOL/HOLCF/IMP/Denotational.thy Fri May 17 11:05:59 2013 +0200 @@ -17,7 +17,7 @@ where "D(SKIP) = (LAM s. Def(undiscr s))" | "D(X ::= a) = (LAM s. Def((undiscr s)(X := aval a (undiscr s))))" -| "D(c0 ; c1) = (dlift(D c1) oo (D c0))" +| "D(c0 ;; c1) = (dlift(D c1) oo (D c0))" | "D(IF b THEN c1 ELSE c2) = (LAM s. if bval b (undiscr s) then (D c1)\s else (D c2)\s)" | "D(WHILE b DO c) =