src/HOL/Tools/Sledgehammer/sledgehammer_reconstructor.ML
changeset 54815 4f6ec8754bf5
parent 54813 c8b04da1bd01
child 54823 a510fc40559c
equal deleted inserted replaced
54814:8911ac4df9c0 54815:4f6ec8754bf5
    13     Metis of string * string |
    13     Metis of string * string |
    14     SMT
    14     SMT
    15 
    15 
    16   datatype play =
    16   datatype play =
    17     Played of reconstructor * Time.time |
    17     Played of reconstructor * Time.time |
    18     Play_Timed_Out of reconstructor * Time.time option |
    18     Play_Timed_Out of reconstructor * Time.time |
    19     Play_Failed of reconstructor
    19     Play_Failed of reconstructor
    20 
    20 
    21   type minimize_command = string list -> string
    21   type minimize_command = string list -> string
    22   type one_line_params = play * string * (string * stature) list * minimize_command * int * int
    22   type one_line_params = play * string * (string * stature) list * minimize_command * int * int
    23 
    23 
    33   Metis of string * string |
    33   Metis of string * string |
    34   SMT
    34   SMT
    35 
    35 
    36 datatype play =
    36 datatype play =
    37   Played of reconstructor * Time.time |
    37   Played of reconstructor * Time.time |
    38   Play_Timed_Out of reconstructor * Time.time option |
    38   Play_Timed_Out of reconstructor * Time.time |
    39   Play_Failed of reconstructor
    39   Play_Failed of reconstructor
    40 
    40 
    41 type minimize_command = string list -> string
    41 type minimize_command = string list -> string
    42 type one_line_params = play * string * (string * stature) list * minimize_command * int * int
    42 type one_line_params = play * string * (string * stature) list * minimize_command * int * int
    43 
    43