src/HOLCF/ex/Dagstuhl.thy
changeset 35642 f478d5a9d238
parent 35174 e15040ae75d7
child 35948 5e7909f0346b
     1.1 --- a/src/HOLCF/ex/Dagstuhl.thy	Sun Mar 07 16:12:01 2010 -0800
     1.2 +++ b/src/HOLCF/ex/Dagstuhl.thy	Sun Mar 07 16:39:31 2010 -0800
     1.3 @@ -52,7 +52,7 @@
     1.4    done
     1.5  
     1.6  lemma wir_moel: "YS = YYS"
     1.7 -  apply (rule stream.take_lemmas)
     1.8 +  apply (rule stream.take_lemma)
     1.9    apply (induct_tac n)
    1.10    apply (simp (no_asm))
    1.11    apply (subst YS_def2)