Lines Matching defs:loop
72 * a rewrite will loop or not. These have been arrived at by trial and
651 (* loop proves each antecedent in turn and propagates
653 fun loop [] = []
654 | loop (ant::rst) =
660 outcome::loop rst'
662 val outcomes = loop ants
892 fun loop [] = (if !monitoring > 0 then
896 | loop (x::rst) =
902 handle HOL_ERR _ => loop rst
904 val thm = loop (boolTheory.TRUTH::context)
913 * also can loop. In which case, use the std_solver. *
932 fun loop [] = solver_err()
933 | loop (x::rst) =
938 handle HOL_ERR _ => loop rst
940 in EQ_MP (SYM th) (loop (boolTheory.TRUTH::context))