Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
deleted redundant line
authorpaulson
Fri, 13 Dec 2002 13:47:13 +0100
changeset 13748 bd4100720833
parent 13747 bf308fcfd08e
child 13749 6844c38d74df
deleted redundant line
src/HOL/GroupTheory/Group.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle