src/HOL/Bali/AxExample.thy
changeset 37956 ee939247b2fb
parent 37138 ee23611b6bf2
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Bali/AxExample.thy	Mon Jul 26 13:50:52 2010 +0200
     1.2 +++ b/src/HOL/Bali/AxExample.thy	Mon Jul 26 17:41:26 2010 +0200
     1.3 @@ -8,10 +8,11 @@
     1.4  imports AxSem Example
     1.5  begin
     1.6  
     1.7 -definition arr_inv :: "st \<Rightarrow> bool" where
     1.8 - "arr_inv \<equiv> \<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>
     1.9 +definition
    1.10 +  arr_inv :: "st \<Rightarrow> bool" where
    1.11 + "arr_inv = (\<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>
    1.12                                values obj (Inl (arr, Base)) = Some (Addr a) \<and>
    1.13 -                              heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>"
    1.14 +                              heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>)"
    1.15  
    1.16  lemma arr_inv_new_obj: 
    1.17  "\<And>a. \<lbrakk>arr_inv s; new_Addr (heap s)=Some a\<rbrakk> \<Longrightarrow> arr_inv (gupd(Inl a\<mapsto>x) s)"