1.1 --- a/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 11 13:59:39 2012 +0200
     1.2 +++ b/src/HOL/TPTP/MaSh_Export.thy	Wed Jul 11 21:43:19 2012 +0200
     1.3 @@ -9,40 +9,66 @@
     1.4  uses "mash_export.ML"
     1.5  begin
     1.6  
     1.7 -sledgehammer_params [provers = e, max_relevant = 500]
     1.8 +sledgehammer_params
     1.9 +  [provers = e, max_relevant = 40, strict, dont_slice, type_enc = poly_guards??,
    1.10 +   lam_trans = combs_and_lifting, timeout = 5, dont_preplay, minimize]
    1.11  
    1.12  ML {*
    1.13  open MaSh_Export
    1.14  *}
    1.15  
    1.16  ML {*
    1.17 -val do_it = false (* switch to "true" to generate the files *);
    1.18 -val thy = @{theory List}
    1.19 +if do_it then
    1.20 +  generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
    1.21 +else
    1.22 +  ()
    1.23  *}
    1.24  
    1.25  ML {*
    1.26 -if do_it then generate_meng_paulson_suggestions @{context} thy "/tmp/mash_meng_paulson_suggestions"
    1.27 -else ()
    1.28 +val do_it = true (* switch to "true" to generate the files *);
    1.29 +val thy = @{theory Nat}
    1.30  *}
    1.31  
    1.32  ML {*
    1.33 -if do_it then generate_mash_commands thy "/tmp/mash_commands"
    1.34 -else ()
    1.35 +if do_it then
    1.36 +  generate_features thy false "/tmp/mash_features"
    1.37 +else
    1.38 +  ()
    1.39  *}
    1.40  
    1.41  ML {*
    1.42 -if do_it then generate_mash_features thy false "/tmp/mash_features"
    1.43 -else ()
    1.44 +if do_it then
    1.45 +  generate_accessibility thy false "/tmp/mash_accessibility"
    1.46 +else
    1.47 +  ()
    1.48  *}
    1.49  
    1.50  ML {*
    1.51 -if do_it then generate_mash_accessibility thy false "/tmp/mash_accessibility"
    1.52 -else ()
    1.53 +if do_it then
    1.54 +  generate_isa_dependencies thy false "/tmp/mash_isa_dependencies"
    1.55 +else
    1.56 +  ()
    1.57  *}
    1.58  
    1.59  ML {*
    1.60 -if do_it then generate_mash_dependencies thy false "/tmp/mash_dependencies"
    1.61 -else ()
    1.62 +if do_it then
    1.63 +  generate_atp_dependencies @{context} thy false "/tmp/mash_atp_dependencies"
    1.64 +else
    1.65 +  ()
    1.66 +*}
    1.67 +
    1.68 +ML {*
    1.69 +if do_it then
    1.70 +  generate_commands thy "/tmp/mash_commands"
    1.71 +else
    1.72 +  ()
    1.73 +*}
    1.74 +
    1.75 +ML {*
    1.76 +if do_it then
    1.77 +  generate_meng_paulson_suggestions @{context} thy 500 "/tmp/mash_meng_paulson_suggestions"
    1.78 +else
    1.79 +  ()
    1.80  *}
    1.81  
    1.82  end