Structure Thm_convs

signature Thm_convs =
sig
   val CONJ_ASSOC_NORM_CONV : Abbrev.conv
   val DISJ_ASSOC_NORM_CONV : Abbrev.conv
   val EQ_EXPAND_CONV : Abbrev.conv
   val IMP_EXPAND_CONV : Abbrev.conv
   val IMP_F_EQ_F_CONV : Abbrev.conv
   val IMP_IMP_CONJ_IMP_CONV : Abbrev.conv
   val LEFT_DIST_NORM_CONV : Abbrev.conv
   val NOT_CONJ_NORM_CONV : Abbrev.conv
   val NOT_DISJ_NORM_CONV : Abbrev.conv
   val NOT_NOT_NORM_CONV : Abbrev.conv
   val OR_F_CONV : Abbrev.conv
   val RIGHT_DIST_NORM_CONV : Abbrev.conv
   val ADD_ASSOC_CONV : Abbrev.conv
   val ADD_SYM_CONV : Abbrev.conv
   val GATHER_BOTH_CONV : Abbrev.conv
   val GATHER_LEFT_CONV : Abbrev.conv
   val GATHER_NEITHER_CONV : Abbrev.conv
   val GATHER_RIGHT_CONV : Abbrev.conv
   val GEQ_NORM_CONV : Abbrev.conv
   val GREAT_NORM_CONV : Abbrev.conv
   val LEFT_ADD_DISTRIB_CONV : Abbrev.conv
   val LESS_NORM_CONV : Abbrev.conv
   val MULT_ASSOC_CONV : Abbrev.conv
   val MULT_COMM_CONV : Abbrev.conv
   val NOT_GEQ_NORM_CONV : Abbrev.conv
   val NOT_GREAT_NORM_CONV : Abbrev.conv
   val NOT_LEQ_NORM_CONV : Abbrev.conv
   val NOT_LESS_NORM_CONV : Abbrev.conv
   val NOT_NUM_EQ_NORM_CONV : Abbrev.conv
   val NUM_EQ_NORM_CONV : Abbrev.conv
   val PLUS_ZERO_CONV : Abbrev.conv
   val SYM_ADD_ASSOC_CONV : Abbrev.conv
   val SYM_ONE_MULT_CONV : Abbrev.conv
   val ZERO_MULT_CONV : Abbrev.conv
   val ZERO_MULT_PLUS_CONV : Abbrev.conv
   val ZERO_PLUS_CONV : Abbrev.conv
   val LEQ_PLUS_CONV : Abbrev.conv
   val FORALL_SIMP_CONV : Abbrev.conv
   val NUM_COND_RATOR_CONV : Abbrev.conv
   val NUM_COND_RAND_CONV : Abbrev.conv
   val SUB_NORM_CONV : Abbrev.conv
   val COND_RATOR_CONV : Abbrev.conv
   val COND_RAND_CONV : Abbrev.conv
   val COND_EXPAND_CONV : Abbrev.conv

end

HOL 4, Kananaskis-10