| Tue, 17 Aug 2010 16:49:51 +0200 | blanchet | invoke Variable.export/import_term on the entire formula, to make sure that schematic variables don't get different indices in different subterms; | file | diff | annotate |
| Mon, 09 Aug 2010 12:05:48 +0200 | blanchet | move Sledgehammer's HOL -> FOL translation to separate file (sledgehammer_translate.ML) | file | diff | annotate |