src/HOL/MicroJava/Comp/LemmasComp.thy
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)