src/HOLCF/One.ML

spassshell and testout.py are used to filter the proof part out of SPASS's
output (i.e. cuts out input and search information).

(* 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";