src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 43085 0a2f5b86bdd7
parent 43064 b6e61d22fa61
child 43100 49347c6354b5
equal deleted inserted replaced
43084:946c8e171ffd 43085:0a2f5b86bdd7
    19 
    19 
    20 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
    20 structure Sledgehammer_Isar : SLEDGEHAMMER_ISAR =
    21 struct
    21 struct
    22 
    22 
    23 open ATP_Systems
    23 open ATP_Systems
       
    24 open ATP_Translate
    24 open Sledgehammer_Util
    25 open Sledgehammer_Util
    25 open Sledgehammer_ATP_Translate
       
    26 open Sledgehammer_Provers
    26 open Sledgehammer_Provers
    27 open Sledgehammer_Minimize
    27 open Sledgehammer_Minimize
    28 open Sledgehammer_Run
    28 open Sledgehammer_Run
    29 
    29 
    30 val sledgehammerN = "sledgehammer"
    30 val sledgehammerN = "sledgehammer"