--- a/src/HOLCF/Fix.ML Wed Jan 29 15:58:17 1997 +0100
+++ b/src/HOLCF/Fix.ML Fri Jan 31 13:57:33 1997 +0100
@@ -398,8 +398,7 @@
(rtac (fixdef RS fix_eq4) 1),
(rtac trans 1),
(rtac beta_cfun 1),
- (cont_tacR 1),
- (rtac refl 1)
+ (Simp_tac 1)
]);
(* use this one for definitions! *)
@@ -411,7 +410,7 @@
(rtac (fix_eq2) 1),
(rtac fixdef 1),
(rtac beta_cfun 1),
- (cont_tacR 1)
+ (Simp_tac 1)
]);
(* ------------------------------------------------------------------------ *)
@@ -1323,6 +1322,8 @@
etac adm_disj 1,
atac 1]);
-val adm_thms = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
+val adm_lemmas = [adm_imp,adm_disj,adm_eq,adm_not_UU,adm_UU_not_less,
adm_all2,adm_not_less,adm_not_free,adm_not_conj,adm_conj,adm_less];
+Addsimps adm_lemmas;
+