Mon, 09 Aug 2010 12:05:48 +0200 | blanchet | move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML) | changeset | files |
Mon, 09 Aug 2010 11:05:45 +0200 | blanchet | fiddle some more with "max_new_relevant_facts_per_iter" | changeset | files |
Mon, 09 Aug 2010 11:03:54 +0200 | blanchet | replace recursion with "fold" | changeset | files |
Mon, 09 Aug 2010 10:39:53 +0200 | blanchet | remove debugging output | changeset | files |
Mon, 09 Aug 2010 10:38:57 +0200 | blanchet | remove now needless "Thm.transfer" | changeset | files |
Mon, 09 Aug 2010 10:13:18 +0200 | blanchet | reintroduced old code that removed axioms from the conjecture assumptions, ported to FOF | changeset | files |
Mon, 09 Aug 2010 09:57:50 +0200 | blanchet | merge | changeset | files |