observe standard convention for syntax consts;
authorwenzelm
Wed Feb 24 21:55:46 2010 +0100 (2010-02-24)
changeset 35352fa051b504c3f
parent 35351 7425aece4ee3
child 35353 1391f82da5a4
observe standard convention for syntax consts;
src/HOL/Hoare/Hoare_Logic_Abort.thy
src/HOL/Library/Multiset.thy
     1.1 --- a/src/HOL/Hoare/Hoare_Logic_Abort.thy	Wed Feb 24 20:37:01 2010 +0100
     1.2 +++ b/src/HOL/Hoare/Hoare_Logic_Abort.thy	Wed Feb 24 21:55:46 2010 +0100
     1.3 @@ -256,8 +256,8 @@
     1.4  (* Special syntax for guarded statements and guarded array updates: *)
     1.5  
     1.6  syntax
     1.7 -  guarded_com :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
     1.8 -  array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70, 65] 61)
     1.9 +  "_guarded_com" :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com"  ("(2_ \<rightarrow>/ _)" 71)
    1.10 +  "_array_update" :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com"  ("(2_[_] :=/ _)" [70, 65] 61)
    1.11  translations
    1.12    "P \<rightarrow> c" == "IF P THEN c ELSE CONST Abort FI"
    1.13    "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
     2.1 --- a/src/HOL/Library/Multiset.thy	Wed Feb 24 20:37:01 2010 +0100
     2.2 +++ b/src/HOL/Library/Multiset.thy	Wed Feb 24 21:55:46 2010 +0100
     2.3 @@ -1502,13 +1502,13 @@
     2.4  by (cases M) auto
     2.5  
     2.6  syntax
     2.7 -  comprehension1_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
     2.8 +  "_comprehension1_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
     2.9        ("({#_/. _ :# _#})")
    2.10  translations
    2.11    "{#e. x:#M#}" == "CONST image_mset (%x. e) M"
    2.12  
    2.13  syntax
    2.14 -  comprehension2_mset :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
    2.15 +  "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
    2.16        ("({#_/ | _ :# _./ _#})")
    2.17  translations
    2.18    "{#e | x:#M. P#}" => "{#e. x :# {# x:#M. P#}#}"