src/HOL/Bali/Example.thy
changeset 28524 644b62cf678f
parent 26480 544cef16045b
child 30235 58d147683393
     1.1 --- a/src/HOL/Bali/Example.thy	Tue Oct 07 16:07:40 2008 +0200
     1.2 +++ b/src/HOL/Bali/Example.thy	Tue Oct 07 16:07:50 2008 +0200
     1.3 @@ -230,7 +230,7 @@
     1.4  lemma table_classes_Object [simp]: 
     1.5   "table_of Classes Object = Some \<lparr>access=Public,cfields=[]
     1.6                                   ,methods=Object_mdecls
     1.7 -                                 ,init=Skip,super=arbitrary,superIfs=[]\<rparr>"
     1.8 +                                 ,init=Skip,super=undefined,superIfs=[]\<rparr>"
     1.9  apply (unfold table_classes_defs)
    1.10  apply (simp (no_asm) add:Object_def)
    1.11  done
    1.12 @@ -1246,13 +1246,13 @@
    1.13    "obj_c"   == "\<lparr>tag=CInst (SXcpt NullPointer),values=CONST empty\<rparr>"
    1.14    "arr_N"   == "CONST empty(Inl (CONST arr, CONST Base)\<mapsto>Null)"
    1.15    "arr_a"   == "CONST empty(Inl (CONST arr, CONST Base)\<mapsto>Addr a)"
    1.16 -  "globs1"  == "CONST empty(Inr (CONST Ext)   \<mapsto>\<lparr>tag=arbitrary, values=CONST empty\<rparr>)
    1.17 -                     (Inr (CONST Base)  \<mapsto>\<lparr>tag=arbitrary, values=arr_N\<rparr>)
    1.18 -                     (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=CONST empty\<rparr>)"
    1.19 -  "globs2"  == "CONST empty(Inr (CONST Ext)   \<mapsto>\<lparr>tag=arbitrary, values=CONST empty\<rparr>)
    1.20 -                     (Inr Object\<mapsto>\<lparr>tag=arbitrary, values=CONST empty\<rparr>)
    1.21 +  "globs1"  == "CONST empty(Inr (CONST Ext)   \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    1.22 +                     (Inr (CONST Base)  \<mapsto>\<lparr>tag=CONST undefined, values=arr_N\<rparr>)
    1.23 +                     (Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)"
    1.24 +  "globs2"  == "CONST empty(Inr (CONST Ext)   \<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    1.25 +                     (Inr Object\<mapsto>\<lparr>tag=CONST undefined, values=CONST empty\<rparr>)
    1.26                       (Inl a\<mapsto>obj_a)
    1.27 -                     (Inr (CONST Base)  \<mapsto>\<lparr>tag=arbitrary, values=arr_a\<rparr>)"
    1.28 +                     (Inr (CONST Base)  \<mapsto>\<lparr>tag=CONST undefined, values=arr_a\<rparr>)"
    1.29    "globs3"  == "globs2(Inl b\<mapsto>obj_b)"
    1.30    "globs8"  == "globs3(Inl c\<mapsto>obj_c)"
    1.31    "locs3"   == "CONST empty(VName (CONST e)\<mapsto>Addr b)"