src/HOL/IMP/Com.thy
author wenzelm
Mon, 20 May 2024 15:43:51 +0200
changeset 80182 29f2b8ff84f3
parent 58889 5b7a9633cfa8
child 80914 d97fdabd9e2b
permissions -rw-r--r--
proper support for "isabelle update -D DIR": avoid accidental exclusion of select_dirs (amending e5dafe9e120f);

section "IMP --- A Simple Imperative Language"

theory Com imports BExp begin

datatype
  com = SKIP 
      | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
      | Seq    com  com         ("_;;/ _"  [60, 61] 60)
      | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
      | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)

end