src/HOLCF/One.ML

removed mk_prodT, mk_not (cf. HOL/hologic.ML);
tuned;

(* legacy ML bindings *)

val Exh_one = thm "Exh_one";
val oneE = thm "oneE";
val dist_less_one = thm "dist_less_one";
val dist_eq_one = thms "dist_eq_one";