| changeset 3461 | 7bf1e7c40a0c |
| parent 3324 | 6b26b886ff69 |
| child 3842 | b55686a7b22c |
--- a/src/HOLCF/ex/Stream.ML Thu Jun 26 10:42:50 1997 +0200 +++ b/src/HOLCF/ex/Stream.ML Thu Jun 26 10:43:15 1997 +0200 @@ -363,7 +363,7 @@ fast_tac (HOL_cs addSIs [stream_finite_UU, stream_finite_lemma1]) 1]); qed_goal "adm_not_stream_finite" thy "adm (%x. ~ stream_finite x)" (fn _ => [ - rtac admI 1, + rtac admI2 1, dtac spec 1, etac contrapos 1, dtac stream_finite_less 1,