# HG changeset patch
# User paulson
# Date 1039783633 -3600
# Node ID bd410072083317fd9e69c562d1d4dc8aba7e09a9
# Parent  bf308fcfd08ecc5c643f38b55da08ee243f937ce
deleted redundant line

diff -r bf308fcfd08e -r bd4100720833 src/HOL/GroupTheory/Group.thy
--- a/src/HOL/GroupTheory/Group.thy	Thu Dec 12 11:38:18 2002 +0100
+++ b/src/HOL/GroupTheory/Group.thy	Fri Dec 13 13:47:13 2002 +0100
@@ -184,8 +184,7 @@
 apply (insert prems) 
 apply (simp add: group_def subgroup_def)
 apply (simp add: semigroup_def group_axioms_def, clarify) 
-apply (intro conjI ballI)
-apply (simp_all add: funcsetI subsetD [of H "carrier G"])
+apply (simp add: funcsetI subsetD [of H "carrier G"])
 apply (blast intro: zero_in_subset)  
 done