--- 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)"
--- 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#}#}"