Lines Matching refs:solver
46 fun appconv (c,UNBOUNDED) solver stk tm = c false solver stk tm
47 | appconv (c,BOUNDED r) solver stk tm = if !r = 0 then failwith "exceeded rewrite bound"
48 else c true solver stk tm before
206 in fn solver => fn stack => fn tm =>
208 val thm = conv solver stack tm
385 fun applythm solver t (bound, th) = let
402 val scond = solver h
420 fun apply {solver,conv,context,stack,relation = (relation,_)} t = let
431 tryfind (applythm (solver stack) lookup_t) matches
563 fun apply {solver,conv,context,stack,relation} tm = let
566 tryfind (fn conv' => conv' solver stack tm) (lookup tm net)