--- a/src/HOLCF/Fix.ML Fri May 31 19:47:23 1996 +0200
+++ b/src/HOLCF/Fix.ML Fri May 31 19:55:19 1996 +0200
@@ -587,7 +587,7 @@
]);
-val adm_flat = flat_imp_chain_finite RS adm_chain_finite;
+bind_thm ("adm_flat", flat_imp_chain_finite RS adm_chain_finite);
(* is_flat(?x::?'a) ==> adm(?P::?'a => bool) *)
qed_goalw "flat_void" Fix.thy [is_flat_def] "is_flat(UU::void)"
@@ -828,7 +828,7 @@
(etac spec 1)
]);
-val adm_all2 = (allI RS adm_all);
+bind_thm ("adm_all2", allI RS adm_all);
qed_goal "adm_subst" Fix.thy
"[|cont t; adm P|] ==> adm(%x. P (t x))"