--- a/src/HOL/Bali/AxExample.thy Mon Jul 26 13:50:52 2010 +0200
+++ b/src/HOL/Bali/AxExample.thy Mon Jul 26 17:41:26 2010 +0200
@@ -8,10 +8,11 @@
imports AxSem Example
begin
-definition arr_inv :: "st \<Rightarrow> bool" where
- "arr_inv \<equiv> \<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>
+definition
+ arr_inv :: "st \<Rightarrow> bool" where
+ "arr_inv = (\<lambda>s. \<exists>obj a T el. globs s (Stat Base) = Some obj \<and>
values obj (Inl (arr, Base)) = Some (Addr a) \<and>
- heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>"
+ heap s a = Some \<lparr>tag=Arr T 2,values=el\<rparr>)"
lemma arr_inv_new_obj:
"\<And>a. \<lbrakk>arr_inv s; new_Addr (heap s)=Some a\<rbrakk> \<Longrightarrow> arr_inv (gupd(Inl a\<mapsto>x) s)"