src/HOL/Tools/Argo/argo_real.ML
2017-01-20 boehmes 2017-01-20 less complex rewriting of Argo expressions: select candidate rewrite rules by analyzing only on the kind of the head expression, then select the applicable rewrite rule using ML pattern matching; keep all normalization code in a single place: modules of decision procedures focus on their core aspects; more normalization for non-linear arithmetic
2016-10-02 wenzelm 2016-10-02 updated headers;
2016-09-29 boehmes 2016-09-29 new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic