Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2004-03-29 18:48:38 -0800 (Mon, 29 Mar 2004)
Revision: 5572
Log message:

      It's a first step towards resource-driven selection of hypotheses (and rules)
      that produce >=-inequalities used by the core of arithT.
      
      Current implementation is somewhatcomplicated I'll try to simplify it later.
      
      Rules that produce more than one main subgoal are not supported yet.
      (e.g. when conlusion was "not equal" it branches into two goals ">" and "<")
      I don't see an elegant solution for it yet.
      
      This commit might degrade overall performance but hopefully not too much.
      
      arith.ml - tiny optimization to avoid double-looping along edges
      from a node to itself.
      

Changes	Path
+7 -1	metaprl/refiner/reflib/arith.ml
+237 -141	metaprl/theories/itt/itt_int_arith.ml
+22 -19	metaprl/theories/itt/itt_int_arith.mli