Lines Matching defs:SUBSET
59 ���!s t (x:'a). ~(x IN s) /\ (t SUBSET s) ==> ~(x IN t)���,
390 ((s UNION t) SUBSET u) = ((s SUBSET u) /\ (t SUBSET u))���,
413 ���!s t r:'a->bool. (s SUBSET t) ==> (s DIFF r SUBSET t DIFF r)���,
427 s1 SUBSET t1 /\ s2 SUBSET t2 ==>
428 (s1 UNION s2) SUBSET (t1 UNION t2)���,
456 ���!s t r:'a->bool. s SUBSET t /\ DISJOINT t r ==> DISJOINT s r���,
492 val SUBSET = save_thm("SUBSET", CONJ EMPTY_SUBSET INSERT_SUBSET);