src/HOL/Bali/State.thy
changeset 28524 644b62cf678f
parent 25511 54db9b5080b8
child 30235 58d147683393
     1.1 --- a/src/HOL/Bali/State.thy	Tue Oct 07 16:07:40 2008 +0200
     1.2 +++ b/src/HOL/Bali/State.thy	Tue Oct 07 16:07:50 2008 +0200
     1.3 @@ -328,7 +328,7 @@
     1.4    init_class_obj :: "prog \<Rightarrow> qtname \<Rightarrow> st \<Rightarrow> st"
     1.5  
     1.6  translations
     1.7 - "init_class_obj G C" == "init_obj G arbitrary (Inr C)"
     1.8 + "init_class_obj G C" == "init_obj G CONST undefined (Inr C)"
     1.9  
    1.10  lemma gupd_def2 [simp]: "gupd(r\<mapsto>obj) (st g l) = st (g(r\<mapsto>obj)) l"
    1.11  apply (unfold gupd_def)