src/HOL/ATP_Linkup.thy
changeset 25741 2d102ddaca8b
parent 25728 71e33d95ac55
child 26729 43a72d892594
equal deleted inserted replaced
25740:de65baf89106 25741:2d102ddaca8b
    17   ("Tools/res_reconstruct.ML")
    17   ("Tools/res_reconstruct.ML")
    18   ("Tools/watcher.ML")
    18   ("Tools/watcher.ML")
    19   ("Tools/res_atp.ML")
    19   ("Tools/res_atp.ML")
    20   ("Tools/res_atp_provers.ML")
    20   ("Tools/res_atp_provers.ML")
    21   ("Tools/res_atp_methods.ML")
    21   ("Tools/res_atp_methods.ML")
    22   "~~/src/Tools/random_word.ML"
       
    23   "~~/src/Tools/Metis/metis.ML"
    22   "~~/src/Tools/Metis/metis.ML"
    24   ("Tools/metis_tools.ML")
    23   ("Tools/metis_tools.ML")
    25 begin
    24 begin
    26 
    25 
    27 definition COMBI :: "'a => 'a"
    26 definition COMBI :: "'a => 'a"