src/HOL/Arith.ML
changeset 6968 7f2977e96a5c
parent 6864 32b5d68196d2
child 6987 4e0defe58b42
equal deleted inserted replaced
6967:a3c163ed1e04 6968:7f2977e96a5c
   863 val sym = sym;
   863 val sym = sym;
   864 val not_lessD = linorder_not_less RS iffD1;
   864 val not_lessD = linorder_not_less RS iffD1;
   865 val not_leD = linorder_not_le RS iffD1;
   865 val not_leD = linorder_not_le RS iffD1;
   866 
   866 
   867 
   867 
   868 fun mk_Eq thm = (thm RS Eq_FalseI) handle _ => (thm RS Eq_TrueI);
   868 fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
   869 
   869 
   870 val mk_Trueprop = HOLogic.mk_Trueprop;
   870 val mk_Trueprop = HOLogic.mk_Trueprop;
   871 
   871 
   872 fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
   872 fun neg_prop(TP$(Const("Not",_)$t)) = TP$t
   873   | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);
   873   | neg_prop(TP$t) = TP $ (Const("Not",HOLogic.boolT-->HOLogic.boolT)$t);