src/Tools/Argo/argo_thy.ML
Sun, 20 Dec 2020 22:04:47 +0100 wenzelm tuned comments;
Fri, 20 Jan 2017 21:05:11 +0100 boehmes 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
Sun, 02 Oct 2016 14:07:43 +0200 wenzelm updated headers;
Thu, 29 Sep 2016 20:54:44 +0200 boehmes new proof method "argo" for a combination of quantifier-free propositional logic with equality and linear real arithmetic
less more (0) tip