# HG changeset patch
# User blanchet
# Date 1358463235 -3600
# Node ID b85cb3049df9a67294ef5072e2d6f2ccefd9340b
# Parent  7a7d1418301e797099f1d8423e12a92510b5e2c2
MeSh prover generation

diff -r 7a7d1418301e -r b85cb3049df9 src/HOL/TPTP/MaSh_Export.thy
--- a/src/HOL/TPTP/MaSh_Export.thy	Thu Jan 17 23:29:22 2013 +0100
+++ b/src/HOL/TPTP/MaSh_Export.thy	Thu Jan 17 23:53:55 2013 +0100
@@ -105,4 +105,12 @@
   ()
 *}
 
+ML {*
+if do_it then
+  generate_mesh_suggestions max_suggestions (prefix ^ "mash_prover_suggestions")
+      (prefix ^ "mepo_suggestions") (prefix ^ "mesh_prover_suggestions")
+else
+  ()
+*}
+
 end