Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOLCF/IMP/Denotational.thy
changeset 5192 704dd3a6d47d
parent 4904 5f6b2dd1cd11
child 9247 ad9f986616de 
--- a/src/HOLCF/IMP/Denotational.thy	Fri Jul 24 13:39:47 1998 +0200
+++ b/src/HOLCF/IMP/Denotational.thy	Fri Jul 24 13:44:27 1998 +0200
@@ -14,7 +14,7 @@
 
 consts D :: "com => state discr -> state lift"
 
-primrec D com
+primrec
   "D(SKIP) = (LAM s. Def(undiscr s))"
   "D(X := a) = (LAM s. Def((undiscr s)[X := a(undiscr s)]))"
   "D(c0 ; c1) = (dlift(D c1) oo (D c0))"
isabelle