author | oheimb |
Thu, 09 Aug 2001 18:51:41 +0200 | |
changeset 11495 | 3621dea6113e |
parent 11494 | 23a118849801 |
child 11496 | fa8d12b789e1 |
--- a/src/HOLCF/ex/Stream.ML Thu Aug 09 18:12:15 2001 +0200 +++ b/src/HOLCF/ex/Stream.ML Thu Aug 09 18:51:41 2001 +0200 @@ -407,7 +407,7 @@ Addsimps [slen_empty, slen_scons]; -Goal "#x < Fin 1 = (x = UU)"; +Goal "#x < Fin 1' = (x = UU)"; by (stream_case_tac "x" 1); by (auto_tac (claset(), simpset() delsimps [thm "iSuc_Fin"] addsimps [thm "Fin_0", thm "iSuc_Fin" RS sym, thm "i0_iless_iSuc", thm "iSuc_mono"]));