src/HOL/IMP/ACom.thy
changeset 45751 f8723843c29e
parent 45746 579fb74aa409
child 46068 b9d4ec0f79ac
equal deleted inserted replaced
45747:8b05cda62000 45751:f8723843c29e
     8 definition "show_state xs s = [(x,s x). x \<leftarrow> xs]"
     8 definition "show_state xs s = [(x,s x). x \<leftarrow> xs]"
     9 
     9 
    10 section "Annotated Commands"
    10 section "Annotated Commands"
    11 
    11 
    12 datatype 'a acom =
    12 datatype 'a acom =
    13   SKIP   'a                           ("SKIP {_}") |
    13   SKIP   'a                           ("SKIP {_}" 61) |
    14   Assign vname aexp 'a                ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
    14   Assign vname aexp 'a                ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
    15   Semi   "('a acom)" "('a acom)"          ("_;//_"  [60, 61] 60) |
    15   Semi   "('a acom)" "('a acom)"          ("_;//_"  [60, 61] 60) |
    16   If     bexp "('a acom)" "('a acom)" 'a
    16   If     bexp "('a acom)" "('a acom)" 'a
    17     ("(IF _/ THEN _/ ELSE _//{_})"  [0, 0, 61, 0] 61) |
    17     ("(IF _/ THEN _/ ELSE _//{_})"  [0, 0, 61, 0] 61) |
    18   While  'a bexp "('a acom)" 'a
    18   While  'a bexp "('a acom)" 'a