src/HOLCF/One.ML
author urbanc
Wed, 02 Nov 2005 15:31:12 +0100
changeset 18067 8b9848d150ba
parent 17838 3032e90c4975
permissions -rw-r--r--
- completed the list of thms for supp_atm - cleaned up the way how thms are collected under single names


(* legacy ML bindings *)

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