# HG changeset patch # User paulson # Date 1142872702 -3600 # Node ID c5d236fe96684fb847a4b05e5bfdc30c1135e7c6 # Parent 871d7aea081a34a96416c5e846d865c3f30f1e97 subsetI is often necessary diff -r 871d7aea081a -r c5d236fe9668 src/HOL/Set.thy --- 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 \ B" +lemma subsetI [atp,intro!]: "(!!x. x:A ==> x:B) ==> A \ B" by (simp add: subset_def) text {*