Preds of polymorphism * type_level * type_heaviness |

     Preds of polymorphism * type_level * type_heaviness |

     Tags of polymorphism * type_level * type_heaviness

     Tags of polymorphism * type_level * type_heaviness

   type translated_formula

   type translated_formula

   val bound_var_prefix : string

   val bound_var_prefix : string

   val schematic_var_prefix: string

   val schematic_var_prefix: string

   val fixed_var_prefix: string

   val fixed_var_prefix: string

   val tvar_prefix: string

   val tvar_prefix: string

   val tfree_prefix: string

   val tfree_prefix: string

   val conjecture_prefix : string

   val conjecture_prefix : string

   val helper_prefix : string

   val helper_prefix : string

   val typed_helper_suffix : string

   val typed_helper_suffix : string

   val predicator_name : string

   val predicator_name : string

   val app_op_name : string

   val app_op_name : string

   val type_pred_name : string

   val type_pred_name : string

   val simple_type_prefix : string

   val simple_type_prefix : string

   val ascii_of: string -> string

   val ascii_of: string -> string

   val unascii_of: string -> string

   val unascii_of: string -> string

   val strip_prefix_and_unascii : string -> string -> string option

   val strip_prefix_and_unascii : string -> string -> string option

 val intro_info = useful_isabelle_info "intro"

 val intro_info = useful_isabelle_info "intro"

 val elim_info = useful_isabelle_info "elim"

 val elim_info = useful_isabelle_info "elim"

 val simp_info = useful_isabelle_info "simp"

 val simp_info = useful_isabelle_info "simp"

 val bound_var_prefix = "B_"

 val bound_var_prefix = "B_"

 val schematic_var_prefix = "V_"

 val schematic_var_prefix = "V_"

 val fixed_var_prefix = "v_"

 val fixed_var_prefix = "v_"

 val tvar_prefix = "T_"

 val tvar_prefix = "T_"

 val typed_helper_suffix = "_T"

 val typed_helper_suffix = "_T"

 val untyped_helper_suffix = "_U"

 val untyped_helper_suffix = "_U"

 val predicator_name = "hBOOL"

 val predicator_name = "hBOOL"

 val app_op_name = "hAPP"

 val app_op_name = "hAPP"

 val type_pred_name = "is"

 val type_pred_name = "is"

 val simple_type_prefix = "ty_"

 val simple_type_prefix = "ty_"

 (* Freshness almost guaranteed! *)

 (* Freshness almost guaranteed! *)

 val sledgehammer_weak_prefix = "Sledgehammer:"

 val sledgehammer_weak_prefix = "Sledgehammer:"