Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
disambiguated := ; added Examples (factorial)
authoroheimb
Wed, 05 Jul 2000 14:26:58 +0200
changeset 9247 ad9f986616de
parent 9246 91423cd08c6f
child 9248 e1dee89de037
disambiguated := ; added Examples (factorial)
src/HOLCF/IMP/Denotational.thy file | annotate | diff | comparison | revisions 
--- 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)"
isabelle