Structure extrealSimps


Source File Identifier index Theory binding index

signature extrealSimps = sig

(* Extended real inequality simps to generally be used with augment_srw_ss *)
val EXTREAL_ss : simpLib.ssfrag;

end


Source File Identifier index Theory binding index

HOL 4, Trindemossen-1