Structure enumTacs
(* File: enumTacs.sig Author: F.L.Morris created 8/17/13 *)
signature enumTacs =
sig
type conv = Abbrev.conv;
type thm = Thm.thm;
type term = Term.term;
type hol_type = Term.hol_type;
val EQ_LESS_CONV: conv;
val COND_EQ_LESS_CONV: conv;
val BL_CONS_CONV: conv;
val bt_rev_CONV: conv;
val bt_to_list_CONV: conv;
val bl_to_bt_CONV: conv;
val list_to_bl_CONV: conv;
val list_to_bt_CONV: conv;
val set_TO_ENUMERAL_CONV: conv -> term -> conv;
val DISPLAY_TO_set_CONV: conv;
val DISPLAY_TO_ENUMERAL_CONV:conv -> term -> conv;
val IN_CONV: conv -> conv;
val OWL_TO_ENUMERAL: thm -> thm;
val ENUMERAL_TO_OWL: conv -> conv;
val set_TO_DISPLAY_CONV: conv;
val ENUMERAL_TO_set_CONV: conv -> conv;
val ENUMERAL_TO_DISPLAY_CONV: conv -> conv;
val TO_set_CONV: conv -> conv;
val OWL_UNION: conv -> thm -> thm -> thm;
val UNION_CONV: conv -> conv;
val OWL_INTER: conv -> thm -> thm -> thm;
val INTER_CONV: conv -> conv;
val OWL_DIFF: conv -> thm -> thm -> thm;
val SET_DIFF_CONV: conv -> conv;
val SET_EXPR_TO_OWL: conv -> term -> thm;
val SET_EXPR_CONV: conv -> conv;
val set_TO_OWL: conv -> term -> term -> thm;
end;
HOL 4, Kananaskis-10