Lines Matching defs:chain
1084 `!c. chain c R ==> upper_bounds c R <> {}`
1445 val chain = new_definition ("chain",
1448 val _ = overload_on ("chain",``Chain``);
1464 ``!r:'a#'a->bool s:'a->bool. chain r s = chain s r``,
1465 REWRITE_TAC [chain, chain_def] THEN SET_TAC []);
1476 (!P. chain P r ==> upper_bounds P r <> {}) ==>
1479 (!P. chain(r) P ==> (?y. fl(r) y /\ !x. P x ==> r(x,y))) ==>
1485 (!t. chain t r ==> upper_bounds t r <> {})
1491 (!P. chain(l) P ==> (?y. fl(l) y /\ !x. P x ==> l(x,y))) ==>
1519 REWRITE_TAC[chain] THEN SIMP_TAC std_ss [IN_DEF] THEN
1530 REWRITE_TAC[chain] THEN SIMP_TAC std_ss [IN_DEF] THEN