src/HOL/Tools/ATP/atp_translate.ML
changeset 43136 cf5cda219058
parent 43130 d73fc2e55308
child 43139 9ed5d8ad8fa0
equal deleted inserted replaced
43135:8c32a0160b0d 43136:cf5cda219058
     7 *)
     7 *)
     8 
     8 
     9 signature ATP_TRANSLATE =
     9 signature ATP_TRANSLATE =
    10 sig
    10 sig
    11   type 'a fo_term = 'a ATP_Problem.fo_term
    11   type 'a fo_term = 'a ATP_Problem.fo_term
       
    12   type connective = ATP_Problem.connective
       
    13   type ('a, 'b, 'c) formula = ('a, 'b, 'c) ATP_Problem.formula
    12   type format = ATP_Problem.format
    14   type format = ATP_Problem.format
    13   type formula_kind = ATP_Problem.formula_kind
    15   type formula_kind = ATP_Problem.formula_kind
    14   type 'a problem = 'a ATP_Problem.problem
    16   type 'a problem = 'a ATP_Problem.problem
    15 
    17 
    16   type name = string * string
    18   type name = string * string
   113   val level_of_type_sys : type_sys -> type_level
   115   val level_of_type_sys : type_sys -> type_level
   114   val is_type_sys_virtually_sound : type_sys -> bool
   116   val is_type_sys_virtually_sound : type_sys -> bool
   115   val is_type_sys_fairly_sound : type_sys -> bool
   117   val is_type_sys_fairly_sound : type_sys -> bool
   116   val choose_format : format list -> type_sys -> format * type_sys
   118   val choose_format : format list -> type_sys -> format * type_sys
   117   val raw_type_literals_for_types : typ list -> type_literal list
   119   val raw_type_literals_for_types : typ list -> type_literal list
       
   120   val mk_aconns :
       
   121     connective -> ('a, 'b, 'c) formula list -> ('a, 'b, 'c) formula
   118   val unmangled_const_name : string -> string
   122   val unmangled_const_name : string -> string
   119   val unmangled_const : string -> string * string fo_term list
   123   val unmangled_const : string -> string * string fo_term list
   120   val translate_atp_fact :
   124   val translate_atp_fact :
   121     Proof.context -> format -> type_sys -> bool -> (string * locality) * thm
   125     Proof.context -> format -> type_sys -> bool -> (string * locality) * thm
   122     -> translated_formula option * ((string * locality) * thm)
   126     -> translated_formula option * ((string * locality) * thm)