src/HOL/Tools/SMT2/smtlib2_interface.ML
changeset 57704 c0da3fc313e3
parent 57553 2a6c31ac1c9a
child 57711 caadd484dec6
equal deleted inserted replaced
57703:fefe3ea75289 57704:c0da3fc313e3
     9 sig
     9 sig
    10   val smtlib2C: SMT2_Util.class
    10   val smtlib2C: SMT2_Util.class
    11   val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
    11   val add_logic: int * (term list -> string option) -> Context.generic -> Context.generic
    12   val translate_config: Proof.context -> SMT2_Translate.config
    12   val translate_config: Proof.context -> SMT2_Translate.config
    13   val assert_index_of_name: string -> int
    13   val assert_index_of_name: string -> int
       
    14   val assert_prefix : string
    14 end;
    15 end;
    15 
    16 
    16 structure SMTLIB2_Interface: SMTLIB2_INTERFACE =
    17 structure SMTLIB2_Interface: SMTLIB2_INTERFACE =
    17 struct
    18 struct
    18 
    19