| changeset 27111 | c19be97e4553 |
| parent 26029 | 46e84ca065f1 |
| child 27291 | 3628064c4b44 |
--- a/src/HOLCF/FOCUS/Fstreams.thy Tue Jun 10 15:31:02 2008 +0200 +++ b/src/HOLCF/FOCUS/Fstreams.thy Tue Jun 10 15:31:03 2008 +0200 @@ -60,7 +60,8 @@ by (simp add: fsingleton_def2) lemma slen_fstreams2[simp]: "#(s ooo <a>) = iSuc (#s)" -apply (case_tac "#s", auto) +apply (cases "#s") +apply (auto simp add: iSuc_Fin) apply (insert slen_sconc [of _ s "Suc 0" "<a>"], auto) by (simp add: sconc_def)