Structure Solve


Source File Identifier index Theory binding index

signature Solve =
sig
   type term = Term.term
   type conv = Abbrev.conv

   val INEQS_FALSE_CONV : conv
   val DISJ_INEQS_FALSE_CONV : conv
   val NOT_NOT_INTRO_CONV : conv
   val is_T : term -> bool
   val is_F : term -> bool
   val NEGATE_CONV : conv -> conv
   val DEPTH_FORALL_CONV : conv -> conv
   val FORALL_ARITH_CONV : conv

end


Source File Identifier index Theory binding index

HOL 4, Trindemossen-1