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/HOL/IMP/Denotation.thy
changeset 1374 5e407f2a3323
parent 1151 c820b3cc3df0
child 1476 608483c2122a 
--- a/src/HOL/IMP/Denotation.thy	Wed Nov 29 16:58:30 1995 +0100
+++ b/src/HOL/IMP/Denotation.thy	Wed Nov 29 17:01:41 1995 +0100
@@ -10,10 +10,10 @@
 
 types com_den = "(state*state)set"
 consts
-  A     :: "aexp => state => nat"
-  B     :: "bexp => state => bool"
-  C     :: "com => com_den"
-  Gamma :: "[bexp,com_den] => (com_den => com_den)"
+  A     :: aexp => state => nat
+  B     :: bexp => state => bool
+  C     :: com => com_den
+  Gamma :: [bexp,com_den] => (com_den => com_den)
 
 primrec A aexp
   A_nat	"A(N(n)) = (%s. n)"
isabelle