src/HOL/IMP/Com.thy
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 45415 bf39b07a7a8e
child 47818 151d137f1095
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 42174
diff changeset
     1
header "IMP --- A Simple Imperative Language"
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     2
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 42174
diff changeset
     3
theory Com imports BExp begin
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     4
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
     5
datatype
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 42174
diff changeset
     6
  com = SKIP 
45321
b227989b6ee6 more IMP text fragments
kleing
parents: 45212
diff changeset
     7
      | Assign vname aexp       ("_ ::= _" [1000, 61] 61)
b227989b6ee6 more IMP text fragments
kleing
parents: 45212
diff changeset
     8
      | Semi   com  com         ("_;/ _"  [60, 61] 60)
43141
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 42174
diff changeset
     9
      | If     bexp com com     ("(IF _/ THEN _/ ELSE _)"  [0, 0, 61] 61)
11fce8564415 Replacing old IMP with new Semantics material
nipkow
parents: 42174
diff changeset
    10
      | While  bexp com         ("(WHILE _/ DO _)"  [0, 61] 61)
924
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    11
806721cfbf46 new version of HOL/IMP with curried function application
clasohm
parents:
diff changeset
    12
end