src/HOL/IMP/Com.thy
author wenzelm
Sat Dec 01 18:52:32 2001 +0100 (2001-12-01)
changeset 12338 de0f4a63baa5
parent 9241 f961c1fdff50
child 12431 07ec657249e5
permissions -rw-r--r--
renamed class "term" to "type" (actually "HOL.type");
     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 = Main +
    11 
    12 types
    13       loc
    14       val   = nat (* or anything else, nat used in examples *)
    15       state = loc => val
    16       aexp  = state => val
    17       bexp  = state => bool
    18 
    19 arities loc :: type
    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