src/Provers/Arith/fast_lin_arith.ML
changeset 35762 af3ff2ba4c54
parent 35693 d58a4ac1ca1c
child 35861 6b4e3b2d33b0
equal deleted inserted replaced
35761:c4a698ee83b4 35762:af3ff2ba4c54
     1 (*  Title:      Provers/Arith/fast_lin_arith.ML
     1 (*  Title:      Provers/Arith/fast_lin_arith.ML
     2     ID:         $Id$
       
     3     Author:     Tobias Nipkow and Tjark Weber and Sascha Boehme
     2     Author:     Tobias Nipkow and Tjark Weber and Sascha Boehme
     4 
     3 
     5 A generic linear arithmetic package.  It provides two tactics
     4 A generic linear arithmetic package.  It provides two tactics
     6 (cut_lin_arith_tac, lin_arith_tac) and a simplification procedure
     5 (cut_lin_arith_tac, lin_arith_tac) and a simplification procedure
     7 (lin_arith_simproc).
     6 (lin_arith_simproc).