Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_proof_reconstruct.ML
changeset 38028 22dcaec5fa77
parent 38027 505657ddb047
child 38033 df99f022751d
equal deleted inserted replaced
38027:505657ddb047 38028:22dcaec5fa77 
    25 end;
 
    25 end;
 
    26 
    26 
    27 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
 
    27 structure Sledgehammer_Proof_Reconstruct : SLEDGEHAMMER_PROOF_RECONSTRUCT =
 
    28 struct
 
    28 struct
 
    29 
    29 
       
    30 open ATP_Problem
 
    30 open Metis_Clauses
 
    31 open Metis_Clauses
 
    31 open Sledgehammer_Util
 
    32 open Sledgehammer_Util
 
    32 open Sledgehammer_Fact_Filter
 
    33 open Sledgehammer_Fact_Filter
 
    33 open ATP_Problem
 
       
    34 
    34 
    35 type minimize_command = string list -> string
 
    35 type minimize_command = string list -> string
 
    36 
    36 
    37 (* Simple simplifications to ensure that sort annotations don't leave a trail of
 
    37 (* Simple simplifications to ensure that sort annotations don't leave a trail of
 
    38    spurious "True"s. *)
 
    38    spurious "True"s. *)
isabelle