# HG changeset patch
# User wenzelm
# Date 1267044946 -3600
# Node ID fa051b504c3f8b8555e920922c7584d692de1619
# Parent  7425aece4ee33ea5d6dd95b673c7e4942541f125
observe standard convention for syntax consts;

diff -r 7425aece4ee3 -r fa051b504c3f src/HOL/Hoare/Hoare_Logic_Abort.thy
--- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Wed Feb 24 20:37:01 2010 +0100
+++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Wed Feb 24 21:55:46 2010 +0100
@@ -256,8 +256,8 @@
 (* Special syntax for guarded statements and guarded array updates: *)
 
 syntax
-  guarded_com :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
-  array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70, 65] 61)
+  "_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
+  "_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70, 65] 61)
 translations
   "P \<rightarrow> c" == "IF P THEN c ELSE CONST Abort FI"
   "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
diff -r 7425aece4ee3 -r fa051b504c3f src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Wed Feb 24 20:37:01 2010 +0100
+++ b/src/HOL/Library/Multiset.thy	Wed Feb 24 21:55:46 2010 +0100
@@ -1502,13 +1502,13 @@
 by (cases M) auto
 
 syntax
-  comprehension1_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
+  "_comprehension1_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
       ("({#_/. _ :# _#})")
 translations
   "{#e. x:#M#}" == "CONST image_mset (%x. e) M"
 
 syntax
-  comprehension2_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
+  "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
       ("({#_/ | _ :# _./ _#})")
 translations
   "{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}"