author | nipkow |
Mon, 09 Feb 1998 14:40:59 +0100 | |
changeset 4612 | 26764de50c74 |
parent 1696 | e84bff5c519b |
child 5183 | 89f162de39cf |
permissions | -rw-r--r-- |
(* Title: HOL/IMP/Com.thy ID: $Id$ Author: Heiko Loetzbeyer & Robert Sandner & Tobias Nipkow, TUM Copyright 1994 TUM Semantics of arithmetic and boolean expressions Syntax of commands *) Com = Arith + types val loc state = "loc => val" aexp = "state => val" bexp = state => bool arities loc,val :: term datatype com = SKIP | ":=" loc aexp (infixl 60) | Semi com com ("_; _" [60, 60] 10) | Cond bexp com com ("IF _ THEN _ ELSE _" 60) | While bexp com ("WHILE _ DO _" 60) end