src/HOL/Library/normarith.ML
2009-08-26 boehmes 2009-08-26 added further conversions and conversionals
2009-06-04 huffman 2009-06-04 add extra type constraints for dist, norm
2009-06-04 huffman 2009-06-04 generalize norm method to work over class real_normed_vector
2009-05-29 huffman 2009-05-29 instance ^ :: (metric_space, finite) metric_space
2009-05-28 huffman 2009-05-28 fix reference to dist_def
2009-05-12 chaieb 2009-05-12 Isolated decision procedure for noms and the general arithmetic solver
2009-04-05 chaieb 2009-04-05 fixed usage of rational constants
2009-03-09 haftmann 2009-03-09 attempt to bypass spurious infix syntax problem on polyml/sun
2009-02-09 chaieb 2009-02-09 Fixed theorem reference
2009-02-09 chaieb 2009-02-09 A generic decision procedure for linear rea arithmetic and normed vector spaces