/[mojave]/metaprl/theories/tactic/tactic_cache.ml
ViewVC logotype

Diff of /metaprl/theories/tactic/tactic_cache.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3583 by nogin, Sun Mar 10 23:29:54 2002 UTC revision 3584 by nogin, Thu Apr 25 15:28:40 2002 UTC
# Line 414  Line 414 
414   *       ext_ftable, and we apply all of them in turn.   *       ext_ftable, and we apply all of them in turn.
415   *          For each rule, this means that we must find an   *          For each rule, this means that we must find an
416   *          instance that applies, which means that we have   *          instance that applies, which means that we have
417   *          to find all hyps that apply.  We do an an exhaustive   *          to find all hyps that apply.  We do an exhaustive
418   *          search through all the inferences we have made in   *          search through all the inferences we have made in
419   *          the current world.  If we find a potential instance,   *          the current world.  If we find a potential instance,
420   *          we apply the forward rule.  If it fails, drop it.   *          we apply the forward rule.  If it fails, drop it.

Legend:
Removed from v.3583  
changed lines
  Added in v.3584

  ViewVC Help
Powered by ViewVC 1.1.26