src/HOL/IMP/Denotation.thy
changeset 1374 5e407f2a3323
parent 1151 c820b3cc3df0
child 1476 608483c2122a
     1.1 --- a/src/HOL/IMP/Denotation.thy	Wed Nov 29 16:58:30 1995 +0100
     1.2 +++ b/src/HOL/IMP/Denotation.thy	Wed Nov 29 17:01:41 1995 +0100
     1.3 @@ -10,10 +10,10 @@
     1.4  
     1.5  types com_den = "(state*state)set"
     1.6  consts
     1.7 -  A     :: "aexp => state => nat"
     1.8 -  B     :: "bexp => state => bool"
     1.9 -  C     :: "com => com_den"
    1.10 -  Gamma :: "[bexp,com_den] => (com_den => com_den)"
    1.11 +  A     :: aexp => state => nat
    1.12 +  B     :: bexp => state => bool
    1.13 +  C     :: com => com_den
    1.14 +  Gamma :: [bexp,com_den] => (com_den => com_den)
    1.15  
    1.16  primrec A aexp
    1.17    A_nat	"A(N(n)) = (%s. n)"