src/HOL/Hoare/Hoare_Logic_Abort.thy
changeset 35352 fa051b504c3f
parent 35320 f80aee1ed475
child 35417 47ee18b6ae32
     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)"