src/HOL/Tools/Sledgehammer/sledgehammer_prover_minimize.ML
changeset 72400 abfeed05c323
parent 69593 3dda49e08b9d
child 73939 9231ea46e041
equal deleted inserted replaced
72399:f8900a5ad4a7 72400:abfeed05c323
    32 
    32 
    33 open ATP_Util
    33 open ATP_Util
    34 open ATP_Proof
    34 open ATP_Proof
    35 open ATP_Problem_Generate
    35 open ATP_Problem_Generate
    36 open ATP_Proof_Reconstruct
    36 open ATP_Proof_Reconstruct
    37 open ATP_Systems
       
    38 open Sledgehammer_Util
    37 open Sledgehammer_Util
    39 open Sledgehammer_Fact
    38 open Sledgehammer_Fact
    40 open Sledgehammer_Proof_Methods
    39 open Sledgehammer_Proof_Methods
    41 open Sledgehammer_Isar
    40 open Sledgehammer_Isar
       
    41 open Sledgehammer_ATP_Systems
    42 open Sledgehammer_Prover
    42 open Sledgehammer_Prover
    43 open Sledgehammer_Prover_ATP
    43 open Sledgehammer_Prover_ATP
    44 open Sledgehammer_Prover_SMT
    44 open Sledgehammer_Prover_SMT
    45 
    45 
    46 fun is_prover_supported ctxt =
    46 fun is_prover_supported ctxt =