# HG changeset patch
# User lcp
# Date 782991268 -3600
# Node ID 6eeff82979df5ec5227538a6b1bb0b45b1172dbb
# Parent  ff4d4d7fcb7f6e63fbd40f421e46236f650041d4
HOL,ZF/IMP/Com.thy: tightening precedences to eliminate syntactic ambiguities.
constructor ";" now yields a low precedence;  the reduction relations are
now more like infixes.

diff -r ff4d4d7fcb7f -r 6eeff82979df src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Fri Oct 21 09:58:05 1994 +0100
+++ b/src/ZF/IMP/Com.thy	Mon Oct 24 10:34:28 1994 +0100
@@ -23,7 +23,7 @@
 
 (** Evaluation of arithmetic expressions **)
 consts  evala    :: "i"
-       "@evala"  :: "[i,i,i] => o"	("<_,_>/ -a-> _")
+       "@evala"  :: "[i,i,i] => o"		("<_,_>/ -a-> _"  [0,0,50] 50)
 translations
     "<ae,sig> -a-> n" == "<ae,sig,n> : evala"
 inductive
@@ -52,7 +52,7 @@
 
 (** Evaluation of boolean expressions **)
 consts evalb	:: "i"	
-       "@evalb" :: "[i,i,i] => o"	("<_,_>/ -b-> _")
+       "@evalb" :: "[i,i,i] => o"		("<_,_>/ -b-> _" [0,0,50] 50)
 
 translations
     "<be,sig> -b-> b" == "<be,sig,b> : evalb"
@@ -81,16 +81,18 @@
 datatype <= "univ(loc Un aexp Un bexp)"
   "com" = skip
         | ":="  ("x:loc", "a:aexp")		(infixl 60)
-        | ";"   ("c0:com", "c1:com")		(infixl 60)
-	| while ("b:bexp", "c:com")		("while _ do _" 60)
-	| ifc   ("b:bexp", "c0:com", "c1:com")	("ifc _ then _ else _" 60)
+        | semic ("c0:com", "c1:com")		("_; _"  [60, 60] 10)
+	| while ("b:bexp", "c:com")		("while _ do _"  60)
+	| ifc   ("b:bexp", "c0:com", "c1:com")	("ifc _ then _ else _"  60)
   type_intrs "aexp.intrs"
 
+(*Constructor ";" has low precedence to avoid syntactic ambiguities
+  with [| m: nat; x: loc; ... |] ==> ...  It usually will need parentheses.*)
 
 (** Execution of commands **)
 consts  evalc    :: "i"
-        "@evalc" :: "[i,i,i] => o"   ("<_,_>/ -c-> _")
-	"assign" :: "[i,i,i] => i"	("_[_'/_]" [900,0,0] 900)
+        "@evalc" :: "[i,i,i] => o"   		("<_,_>/ -c-> _" [0,0,50] 50)
+	"assign" :: "[i,i,i] => i"   		("_[_'/_]"       [95,0,0] 95)
 
 translations
        "<ce,sig> -c-> s" == "<ce,sig,s> : evalc"