File ‹util_base.ML›
signature BASIC_UTIL_BASE =
sig
val boolT: typ
val dest_eq: term -> term * term
val cdest_eq: cterm -> cterm * cterm
val mk_eq: term * term -> term
val is_eq_term: term -> bool
val bFalse: term
val bTrue: term
val true_th: thm
end;
signature UTIL_BASE =
sig
include BASIC_UTIL_BASE
val mk_setT: typ -> typ
val Trueprop_name: string
val Not_name: string
val Conj_name: string
val Disj_name: string
val Imp_name: string
val All_name: string
val Ex_name: string
val is_if: term -> bool
val cTrueprop: cterm
val cNot: cterm
val cConj: cterm
val cDisj: cterm
val to_meta_eq_cv: conv
val to_obj_eq_cv: conv
val to_obj_eq_iff: thm -> thm
val obj_sym_cv: conv
val iffD_th: thm
val nn_create_th: thm
val nn_cancel_th: thm
val to_contra_form_th: thm
val to_contra_form_th': thm
val atomize_imp_th: thm
val atomize_all_th: thm
val conjunct1_th: thm
val conjunct2_th: thm
val conjI_th: thm
val or_intro1_th: thm
val or_intro2_th: thm
val iffD1_th: thm
val iffD2_th: thm
val inv_back_th: thm
val sym_th: thm
val exE_th': thm
val eq_True_th: thm
val eq_True_inv_th: thm
val disj_True1_th: thm
val disj_True2_th: thm
val ex_vardef_th: thm
val imp_conv_disj_th: thm
val de_Morgan_conj_th: thm
val de_Morgan_disj_th: thm
val not_ex_th: thm
val not_all_th: thm
val not_imp_th: thm
val or_cancel1_th: thm
val or_cancel2_th: thm
val swap_all_disj_th: thm
val swap_ex_conj_th: thm
val all_trivial_th: thm
val case_split_th: thm
val atomize_conjL_th: thm
val backward_conv_th: thm
val backward1_conv_th: thm
val backward2_conv_th: thm
val resolve_conv_th: thm
val contra_triv_th: thm
val conj_assoc_th: thm
val conj_commute_th: thm
val disj_assoc_th: thm
val disj_commute_th: thm
val Mem_name: string
val Ball_name: string
val Bex_name: string
val Bex_def_th: thm
val Ball_def_th: thm
end