| changeset 28524 | 644b62cf678f |
| parent 24783 | 5a3e336a2e37 |
| child 33954 | 1bc3b688548c |
--- a/src/HOL/MicroJava/J/Example.thy Tue Oct 07 16:07:40 2008 +0200 +++ b/src/HOL/MicroJava/J/Example.thy Tue Oct 07 16:07:50 2008 +0200 @@ -137,7 +137,7 @@ done declare map_of_Cons [simp del] -- "sic!" -lemma class_tprg_Object [simp]: "class tprg Object = Some (arbitrary, [], [])" +lemma class_tprg_Object [simp]: "class tprg Object = Some (undefined, [], [])" apply (unfold ObjectC_def class_def) apply (simp (no_asm)) done