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