src/HOL/Tools/Sledgehammer/sledgehammer_prover.ML
changeset 55345 8a53ee72e595
parent 55323 253a029335a2
child 55452 29ec8680e61f
equal deleted inserted replaced
55344:a593712f6878 55345:8a53ee72e595
   185     Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
   185     Auto_Try => "Auto Sledgehammer (" ^ quote name ^ ") found a proof"
   186   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   186   | Try => "Sledgehammer (" ^ quote name ^ ") found a proof"
   187   | _ => "Try this")
   187   | _ => "Try this")
   188 
   188 
   189 fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
   189 fun bunch_of_proof_methods smt_proofs needs_full_types desperate_lam_trans =
   190   [Metis_Method (SOME full_type_enc, NONE)] @
       
   191   (if needs_full_types then
   190   (if needs_full_types then
   192      [Metis_Method (SOME full_type_enc, NONE),
   191      [Metis_Method (SOME full_typesN, NONE),
   193       Metis_Method (SOME really_full_type_enc, NONE),
   192       Metis_Method (SOME really_full_type_enc, NONE),
   194       Metis_Method (SOME full_type_enc, SOME desperate_lam_trans)]
   193       Metis_Method (SOME full_typesN, SOME desperate_lam_trans),
       
   194       Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]
   195    else
   195    else
   196      [Metis_Method (NONE, NONE),
   196      [Metis_Method (NONE, NONE),
   197       Metis_Method (SOME no_typesN, SOME desperate_lam_trans)]) @
   197       Metis_Method (SOME full_typesN, NONE),
   198   [Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)] @
   198       Metis_Method (SOME no_typesN, SOME desperate_lam_trans),
       
   199       Metis_Method (SOME really_full_type_enc, SOME desperate_lam_trans)]) @
   199   (if smt_proofs then [SMT_Method] else [])
   200   (if smt_proofs then [SMT_Method] else [])
   200 
   201 
   201 fun extract_proof_method ({type_enc, lam_trans, ...} : params)
   202 fun extract_proof_method ({type_enc, lam_trans, ...} : params)
   202       (Metis_Method (type_enc', lam_trans')) =
   203       (Metis_Method (type_enc', lam_trans')) =
   203     let
   204     let