src/HOL/IMP/Com.thy
changeset 9241 f961c1fdff50
parent 8029 05446a898852
child 12338 de0f4a63baa5
     1.1 --- a/src/HOL/IMP/Com.thy	Tue Jul 04 10:54:32 2000 +0200
     1.2 +++ b/src/HOL/IMP/Com.thy	Tue Jul 04 10:54:46 2000 +0200
     1.3 @@ -9,18 +9,18 @@
     1.4  
     1.5  Com = Main +
     1.6  
     1.7 -types 
     1.8 -      val
     1.9 +types
    1.10        loc
    1.11 -      state = "loc => val"
    1.12 -      aexp  = "state => val"
    1.13 +      val   = nat (* or anything else, nat used in examples *)
    1.14 +      state = loc => val
    1.15 +      aexp  = state => val
    1.16        bexp  = state => bool
    1.17  
    1.18 -arities loc,val :: term
    1.19 +arities loc :: term
    1.20  
    1.21  datatype
    1.22    com = SKIP
    1.23 -      | ":="  loc aexp         (infixl  60)
    1.24 +      | ":=="  loc aexp         (infixl  60)
    1.25        | Semi  com com          ("_; _"  [60, 60] 10)
    1.26        | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
    1.27        | While bexp com         ("WHILE _ DO _"  60)