--- a/src/HOLCF/Fix.ML Fri Jun 03 23:30:31 2005 +0200
+++ b/src/HOLCF/Fix.ML Fri Jun 03 23:33:48 2005 +0200
@@ -11,17 +11,11 @@
val chain_iterate = thm "chain_iterate";
val Ifix_eq = thm "Ifix_eq";
val Ifix_least = thm "Ifix_least";
-val monofun_iterate = thm "monofun_iterate";
-val contlub_iterate = thm "contlub_iterate";
-val cont_iterate = thm "cont_iterate";
+val cont_iterate1 = thm "cont_iterate1";
+val cont_iterate2 = thm "cont_iterate2";
val monofun_iterate2 = thm "monofun_iterate2";
val contlub_iterate2 = thm "contlub_iterate2";
-val cont_iterate2 = thm "cont_iterate2";
-val monofun_Ifix = thm "monofun_Ifix";
-(*val chain_iterate_lub = thm "chain_iterate_lub";*)
-(*val contlub_Ifix_lemma1 = thm "contlub_Ifix_lemma1";*)
-(*val ex_lub_iterate = thm "ex_lub_iterate";*)
-val contlub_Ifix = thm "contlub_Ifix";
+val cont_iterate = thm "cont_iterate";
val cont_Ifix = thm "cont_Ifix";
val fix_eq = thm "fix_eq";
val fix_least = thm "fix_least";
@@ -30,9 +24,7 @@
val fix_eq3 = thm "fix_eq3";
val fix_eq4 = thm "fix_eq4";
val fix_eq5 = thm "fix_eq5";
-val Ifix_def2 = thm "Ifix_def2";
val fix_def2 = thm "fix_def2";
-val admw_def2 = thm "admw_def2";
val def_fix_ind = thm "def_fix_ind";
val adm_impl_admw = thm "adm_impl_admw";
val fix_ind = thm "fix_ind";