src/HOL/Library/normarith.ML
2009-10-21 haftmann 2009-10-21 merged
2009-10-21 haftmann 2009-10-21 curried union as canonical list operation
2009-10-21 haftmann 2009-10-21 removed old-style \ and \\ infixes
2009-10-21 haftmann 2009-10-21 merged
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-10-14 wenzelm 2009-10-14 eliminated obsolete C/flip combinator;
2009-10-01 Philipp Meyer 2009-10-01 additional fixes in normarith.ML due to FuncFun and FuncUtil changes
2009-09-21 Philipp Meyer 2009-09-21 sos method generates and uses proof certificates
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