Structure Theorems

signature Theorems =
sig
   val ONE_PLUS : Thm.thm
   val ZERO_PLUS : Thm.thm
   val PLUS_ZERO : Thm.thm
   val SUC_ADD1 : Thm.thm
   val SUC_ADD2 : Thm.thm
   val ZERO_MULT : Thm.thm
   val MULT_ZERO : Thm.thm
   val ONE_MULT : Thm.thm
   val MULT_ONE : Thm.thm
   val MULT_SUC : Thm.thm
   val MULT_COMM : Thm.thm
   val SUC_ADD_LESS_EQ_F : Thm.thm
   val MULT_LEQ_SUC : Thm.thm
   val ZERO_LESS_EQ_T : Thm.thm
   val SUC_LESS_EQ_ZERO_F : Thm.thm
   val ZERO_LESS_EQ_ONE_TIMES : Thm.thm
   val LESS_EQ_PLUS : Thm.thm
   val LESS_EQ_TRANSIT : Thm.thm
   val NOT_T_F : Thm.thm
   val NOT_F_T : Thm.thm
end

HOL 4, Kananaskis-14