--- a/src/HOLCF/Cfun.ML Thu May 26 02:26:28 2005 +0200
+++ b/src/HOLCF/Cfun.ML Thu May 26 04:41:56 2005 +0200
@@ -71,9 +71,10 @@
val strictify1 = thm "strictify1";
val strictify2 = thm "strictify2";
val chfin_Rep_CFunR = thm "chfin_Rep_CFunR";
-val iso_strict = thm "iso_strict";
-val isorep_defined = thm "isorep_defined";
-val isoabs_defined = thm "isoabs_defined";
+val retraction_strict = thm "retraction_strict";
+val injection_eq = thm "injection_eq";
+val injection_defined_rev = thm "injection_defined_rev";
+val injection_defined = thm "injection_defined";
val chfin2chfin = thm "chfin2chfin";
val flat2flat = thm "flat2flat";
val flat_codom = thm "flat_codom";