src/HOL/Tools/ATP_Manager/atp_systems.ML
changeset 38019 e207a64e1e0b
parent 38017 3ad3e3ca2451
child 38021 e024504943d1
equal deleted inserted replaced
38018:ee6c11ae8077 38019:e207a64e1e0b
    20 struct
    20 struct
    21 
    21 
    22 open Metis_Clauses
    22 open Metis_Clauses
    23 open Sledgehammer_Util
    23 open Sledgehammer_Util
    24 open Sledgehammer_Fact_Filter
    24 open Sledgehammer_Fact_Filter
    25 open Sledgehammer_TPTP_Format
    25 open ATP_Problem
    26 open Sledgehammer_Proof_Reconstruct
    26 open Sledgehammer_Proof_Reconstruct
    27 open ATP_Manager
    27 open ATP_Manager
    28 
    28 
    29 val trace = Unsynchronized.ref false
    29 val trace = Unsynchronized.ref false
    30 fun trace_msg msg = if !trace then tracing (msg ()) else ()
    30 fun trace_msg msg = if !trace then tracing (msg ()) else ()