changeset 48234 | 06216c789ac9 |
child 48235 | 40655464a93b |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/TPTP/mash_import.ML Tue Jul 10 23:36:03 2012 +0200 @@ -0,0 +1,15 @@ +(* Title: HOL/TPTP/mash_import.ML + Author: Jasmin Blanchette, TU Muenchen + Copyright 2012 + +Import proof suggestions from MaSh (Machine-learning for Sledgehammer) and +evaluate them. +*) + +signature MASH_IMPORT = +sig +end; + +structure MaSh_Import : MASH_IMPORT = +struct +end;