Lines Matching defs:IN
50 ���!s (x:'a) y. (x IN s) /\ ~(y IN s) ==> ~(x = y)���,
59 ���!s t (x:'a). ~(x IN s) /\ (t SUBSET s) ==> ~(x IN t)���,
70 ((x IN s ==> ~(x IN t)) /\
71 (x IN t ==> ~(x IN s)))���,
321 (!x. (x IN s) ==> (ss x = x)) /\ ONE_ONE ss ==>
322 ((ss z IN s) = (z IN s))���,
341 ���!s. FINITE s ==> !(x:'a). x IN s ==> (0 < CARD s)���,
441 ���!s t (x:'a). DISJOINT s (x INSERT t) = (DISJOINT s t /\ ~(x IN s))���,
484 val IN = save_thm("IN", CONJ NOT_IN_EMPTY IN_INSERT);
508 ?t. !x. x IN t = ?si. si IN s /\ x IN si���),
510 THEN EXISTS_TAC ���\x:'a. ?si. si IN s /\ x IN si���
531 REWRITE_TAC [EXTENSION, IN_UNION_SET, IN]
537 REWRITE_TAC [EXTENSION, IN_UNION_SET, IN_UNION, IN]
578 ���!s. (UNION_SET s = {}) = (!si:'a->bool. si IN s ==> (si = {}))���,
579 REWRITE_TAC[EXTENSION,IN,IN_UNION_SET]
598 THEN REWRITE_TAC[IN,IN_UNION_SET]
612 [ ASM_REWRITE_TAC[EXTENSION,IN],
629 THEN REWRITE_TAC[IN]
645 UNION_SET {si DELETE e | si IN s} = (UNION_SET s) DELETE e���,
671 (([], ���!s. FINITE s ==> (!si:'a->bool. si IN s ==> FINITE si) ==>
674 THEN REWRITE_TAC[IN,UNION_SET,FINITE_EMPTY,FINITE_UNION]
691 ���!s. FINITE s /\ (!si:'a->bool. si IN s ==> FINITE si) ==>
701 (!si:'a->bool. si IN s ==> FINITE si)���),
719 (FINITE (UNION_SET s) = (!si. si IN s ==> FINITE si))���,
733 (([], ���!s (e:'a). ({si DELETE e | si IN s} = {}) = (s = {})���),
738 THEN REWRITE_TAC[IN]
760 THEN REWRITE_TAC[IN]