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.
subsetI is often necessary
authorpaulson
Mon, 20 Mar 2006 17:38:22 +0100
changeset 19295 c5d236fe9668
parent 19294 871d7aea081a
child 19296 ad96f1095dca
subsetI is often necessary
src/HOL/Set.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Set.thy	Mon Mar 20 17:37:11 2006 +0100
+++ b/src/HOL/Set.thy	Mon Mar 20 17:38:22 2006 +0100
@@ -474,7 +474,7 @@
 
 subsubsection {* Subsets *}
 
-lemma subsetI [intro!]: "(!!x. x:A ==> x:B) ==> A \<subseteq> B"
+lemma subsetI [atp,intro!]: "(!!x. x:A ==> x:B) ==> A \<subseteq> B"
   by (simp add: subset_def)
 
 text {*
isabelle