| changeset 48562 | f6d6d58fa318 |
| parent 46226 | e88e980ed735 |
| child 52857 | 64e3374d5014 |
--- a/src/HOL/MicroJava/Comp/LemmasComp.thy Fri Jul 27 19:27:21 2012 +0200 +++ b/src/HOL/MicroJava/Comp/LemmasComp.thy Fri Jul 27 19:57:23 2012 +0200 @@ -369,9 +369,6 @@ prefer 2 apply assumption apply (simp add: comp_method [of G D]) apply (erule exE)+ -apply (subgoal_tac "z =(fst z, fst (snd z), snd (snd z))") -apply (rule exI) -apply (simp) apply (simp add: split_paired_all) apply (intro strip) apply (simp add: comp_method)