| changeset 13524 | 604d0f3622d6 |
| parent 12030 | 46d57d0290a2 |
| child 14981 | e73f8140af78 |
--- a/src/HOLCF/Fix.ML Tue Aug 27 11:03:02 2002 +0200 +++ b/src/HOLCF/Fix.ML Tue Aug 27 11:03:05 2002 +0200 @@ -697,10 +697,6 @@ by (atac 1); qed "adm_disj"; - -bind_thm("adm_lemma11",adm_lemma11); -bind_thm("adm_disj",adm_disj); - Goal "[| adm(%x.~(P x)); adm Q |] ==> adm(%x. P x --> Q x)"; by (subgoal_tac "(%x. P x --> Q x) = (%x. ~P x | Q x)" 1); by (etac ssubst 1);