src/HOL/IMP/Com.thy
author nipkow
Sat Apr 27 18:47:31 1996 +0200 (1996-04-27)
changeset 1696 e84bff5c519b
parent 1481 03f096efa26d
child 5183 89f162de39cf
permissions -rw-r--r--
A completely new version of IMP.
     1 (*  Title:      HOL/IMP/Com.thy
     2     ID:         $Id$
     3     Author:     Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM
     4     Copyright   1994 TUM
     5 
     6 Semantics of arithmetic and boolean expressions
     7 Syntax of commands
     8 *)
     9 
    10 Com = Arith +
    11 
    12 types 
    13       val
    14       loc
    15       state = "loc => val"
    16       aexp  = "state => val"
    17       bexp  = state => bool
    18 
    19 arities loc,val :: term
    20 
    21 datatype
    22   com = SKIP
    23       | ":="  loc aexp         (infixl  60)
    24       | Semi  com com          ("_; _"  [60, 60] 10)
    25       | Cond  bexp com com     ("IF _ THEN _ ELSE _"  60)
    26       | While bexp com         ("WHILE _ DO _"  60)
    27 
    28 end