| changeset 16314 | 7102a1aaecfd |
| parent 16209 | 36ee7f6af79f |
| child 16699 | 24b494ff8f0f |
--- a/src/HOLCF/Cfun.ML Tue Jun 07 20:04:41 2005 +0200 +++ b/src/HOLCF/Cfun.ML Wed Jun 08 00:04:38 2005 +0200 @@ -57,6 +57,7 @@ val chfin_Rep_CFunR = thm "chfin_Rep_CFunR"; val retraction_strict = thm "retraction_strict"; val injection_eq = thm "injection_eq"; +val injection_less = thm "injection_less"; val injection_defined_rev = thm "injection_defined_rev"; val injection_defined = thm "injection_defined"; val chfin2chfin = thm "chfin2chfin";