changeset 28524 | 644b62cf678f |
parent 24019 | 67bde7cfcf10 |
child 30235 | 58d147683393 |
--- a/src/HOL/Bali/WellForm.thy Tue Oct 07 16:07:40 2008 +0200 +++ b/src/HOL/Bali/WellForm.thy Tue Oct 07 16:07:50 2008 +0200 @@ -562,7 +562,7 @@ lemma class_Object [simp]: "wf_prog G \<Longrightarrow> class G Object = Some \<lparr>access=Public,cfields=[],methods=Object_mdecls, - init=Skip,super=arbitrary,superIfs=[]\<rparr>" + init=Skip,super=undefined,superIfs=[]\<rparr>" apply (unfold wf_prog_def Let_def ObjectC_def) apply (fast dest!: map_of_SomeI) done