enforce parantheses around SKIP {_}
authornipkow
Mon, 05 Dec 2011 07:31:00 +0100
changeset 45751 f8723843c29e
parent 45747 8b05cda62000
child 45752 b5db02fa9536
enforce parantheses around SKIP {_}
src/HOL/IMP/ACom.thy
--- a/src/HOL/IMP/ACom.thy	Sun Dec 04 18:29:29 2011 +0100
+++ b/src/HOL/IMP/ACom.thy	Mon Dec 05 07:31:00 2011 +0100
@@ -10,7 +10,7 @@
 section "Annotated Commands"
 
 datatype 'a acom =
-  SKIP   'a                           ("SKIP {_}") |
+  SKIP   'a                           ("SKIP {_}" 61) |
   Assign vname aexp 'a                ("(_ ::= _/ {_})" [1000, 61, 0] 61) |
   Semi   "('a acom)" "('a acom)"          ("_;//_"  [60, 61] 60) |
   If     bexp "('a acom)" "('a acom)" 'a