1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 18 08:44:04 2012 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Wed Jul 18 08:44:04 2012 +0200
     1.3 @@ -18,27 +18,28 @@
     1.4    datatype mode = Auto_Try | Try | Normal | Auto_Minimize | Minimize
     1.5  
     1.6    type params =
     1.7 -    {debug: bool,
     1.8 -     verbose: bool,
     1.9 -     overlord: bool,
    1.10 -     blocking: bool,
    1.11 -     provers: string list,
    1.12 -     type_enc: string option,
    1.13 -     strict: bool,
    1.14 -     lam_trans: string option,
    1.15 -     uncurried_aliases: bool option,
    1.16 -     fact_filter: string option,
    1.17 -     max_facts: int option,
    1.18 -     fact_thresholds: real * real,
    1.19 -     max_mono_iters: int option,
    1.20 -     max_new_mono_instances: int option,
    1.21 -     isar_proof: bool,
    1.22 -     isar_shrink_factor: int,
    1.23 -     slice: bool,
    1.24 -     minimize: bool option,
    1.25 -     timeout: Time.time,
    1.26 -     preplay_timeout: Time.time,
    1.27 -     expect: string}
    1.28 +    {debug : bool,
    1.29 +     verbose : bool,
    1.30 +     overlord : bool,
    1.31 +     blocking : bool,
    1.32 +     provers : string list,
    1.33 +     type_enc : string option,
    1.34 +     strict : bool,
    1.35 +     lam_trans : string option,
    1.36 +     uncurried_aliases : bool option,
    1.37 +     learn : bool,
    1.38 +     fact_filter : string option,
    1.39 +     max_facts : int option,
    1.40 +     fact_thresholds : real * real,
    1.41 +     max_mono_iters : int option,
    1.42 +     max_new_mono_instances : int option,
    1.43 +     isar_proof : bool,
    1.44 +     isar_shrink_factor : int,
    1.45 +     slice : bool,
    1.46 +     minimize : bool option,
    1.47 +     timeout : Time.time,
    1.48 +     preplay_timeout : Time.time,
    1.49 +     expect : string}
    1.50  
    1.51    type relevance_fudge =
    1.52      {local_const_multiplier : real,
    1.53 @@ -66,19 +67,19 @@
    1.54      SMT_Weighted_Fact of (string * stature) * (int option * thm)
    1.55  
    1.56    type prover_problem =
    1.57 -    {state: Proof.state,
    1.58 -     goal: thm,
    1.59 -     subgoal: int,
    1.60 -     subgoal_count: int,
    1.61 -     facts: prover_fact list}
    1.62 +    {state : Proof.state,
    1.63 +     goal : thm,
    1.64 +     subgoal : int,
    1.65 +     subgoal_count : int,
    1.66 +     facts : prover_fact list}
    1.67  
    1.68    type prover_result =
    1.69 -    {outcome: failure option,
    1.70 -     used_facts: (string * stature) list,
    1.71 -     run_time: Time.time,
    1.72 -     preplay: unit -> play,
    1.73 -     message: play -> string,
    1.74 -     message_tail: string}
    1.75 +    {outcome : failure option,
    1.76 +     used_facts : (string * stature) list,
    1.77 +     run_time : Time.time,
    1.78 +     preplay : unit -> play,
    1.79 +     message : play -> string,
    1.80 +     message_tail : string}
    1.81  
    1.82    type prover =
    1.83      params -> ((string * string list) list -> string -> minimize_command)
    1.84 @@ -306,27 +307,28 @@
    1.85  (** problems, results, ATPs, etc. **)
    1.86  
    1.87  type params =
    1.88 -  {debug: bool,
    1.89 -   verbose: bool,
    1.90 -   overlord: bool,
    1.91 -   blocking: bool,
    1.92 -   provers: string list,
    1.93 -   type_enc: string option,
    1.94 -   strict: bool,
    1.95 -   lam_trans: string option,
    1.96 -   uncurried_aliases: bool option,
    1.97 -   fact_filter: string option,
    1.98 -   max_facts: int option,
    1.99 -   fact_thresholds: real * real,
   1.100 -   max_mono_iters: int option,
   1.101 -   max_new_mono_instances: int option,
   1.102 -   isar_proof: bool,
   1.103 -   isar_shrink_factor: int,
   1.104 -   slice: bool,
   1.105 -   minimize: bool option,
   1.106 -   timeout: Time.time,
   1.107 -   preplay_timeout: Time.time,
   1.108 -   expect: string}
   1.109 +  {debug : bool,
   1.110 +   verbose : bool,
   1.111 +   overlord : bool,
   1.112 +   blocking : bool,
   1.113 +   provers : string list,
   1.114 +   type_enc : string option,
   1.115 +   strict : bool,
   1.116 +   lam_trans : string option,
   1.117 +   uncurried_aliases : bool option,
   1.118 +   learn : bool,
   1.119 +   fact_filter : string option,
   1.120 +   max_facts : int option,
   1.121 +   fact_thresholds : real * real,
   1.122 +   max_mono_iters : int option,
   1.123 +   max_new_mono_instances : int option,
   1.124 +   isar_proof : bool,
   1.125 +   isar_shrink_factor : int,
   1.126 +   slice : bool,
   1.127 +   minimize : bool option,
   1.128 +   timeout : Time.time,
   1.129 +   preplay_timeout : Time.time,
   1.130 +   expect : string}
   1.131  
   1.132  type relevance_fudge =
   1.133    {local_const_multiplier : real,
   1.134 @@ -354,19 +356,19 @@
   1.135    SMT_Weighted_Fact of (string * stature) * (int option * thm)
   1.136  
   1.137  type prover_problem =
   1.138 -  {state: Proof.state,
   1.139 -   goal: thm,
   1.140 -   subgoal: int,
   1.141 -   subgoal_count: int,
   1.142 -   facts: prover_fact list}
   1.143 +  {state : Proof.state,
   1.144 +   goal : thm,
   1.145 +   subgoal : int,
   1.146 +   subgoal_count : int,
   1.147 +   facts : prover_fact list}
   1.148  
   1.149  type prover_result =
   1.150 -  {outcome: failure option,
   1.151 -   used_facts: (string * stature) list,
   1.152 -   run_time: Time.time,
   1.153 -   preplay: unit -> play,
   1.154 -   message: play -> string,
   1.155 -   message_tail: string}
   1.156 +  {outcome : failure option,
   1.157 +   used_facts : (string * stature) list,
   1.158 +   run_time : Time.time,
   1.159 +   preplay : unit -> play,
   1.160 +   message : play -> string,
   1.161 +   message_tail : string}
   1.162  
   1.163  type prover =
   1.164    params -> ((string * string list) list -> string -> minimize_command)