blanchet [Fri, 17 Sep 2010 16:38:11 +0200] rev 39745
merged
blanchet [Fri, 17 Sep 2010 01:59:43 +0200] rev 39744
update README
blanchet [Fri, 17 Sep 2010 01:59:30 +0200] rev 39743
regenerate "metis.ML"
blanchet [Fri, 17 Sep 2010 01:58:21 +0200] rev 39742
fix license
blanchet [Fri, 17 Sep 2010 01:56:19 +0200] rev 39741
updated source files with Metis 2.3 (timestamp: 16 Sept. 2010)
blanchet [Fri, 17 Sep 2010 01:22:01 +0200] rev 39740
move functions around
blanchet [Fri, 17 Sep 2010 00:54:56 +0200] rev 39739
simplify Skolem handling;
things are much easier now that Sledgehammer doesn't skolemize, only Metis
blanchet [Fri, 17 Sep 2010 00:35:19 +0200] rev 39738
make "subst_translation" more robust w.r.t. type instantiations like {_1234 |-> 'a}
blanchet [Thu, 16 Sep 2010 17:30:29 +0200] rev 39737
complete refactoring of Metis along the lines of Sledgehammer
blanchet [Thu, 16 Sep 2010 16:54:42 +0200] rev 39736
got caught once again by SML's pattern maching (ctor vs. var)