src/HOLCF/ex/Stream.thy
changeset 29855 e0ab6cf95539
parent 29530 9905b660612b
child 30807 a167ed35ec0d
     1.1 --- a/src/HOLCF/ex/Stream.thy	Tue Feb 10 09:58:58 2009 +0000
     1.2 +++ b/src/HOLCF/ex/Stream.thy	Tue Feb 10 10:25:09 2009 +0000
     1.3 @@ -252,7 +252,9 @@
     1.4  lemma stream_finite_ind2:
     1.5  "[| P UU; !! x. x ~= UU ==> P (x && UU); !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s )|] ==>
     1.6                                   !s. P (stream_take n$s)"
     1.7 -apply (rule nat_induct2 [of _ n],auto)
     1.8 +apply (rule nat_less_induct [of _ n],auto)
     1.9 +apply (case_tac n, auto) 
    1.10 +apply (case_tac nat, auto) 
    1.11  apply (case_tac "s=UU",clarsimp)
    1.12  apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
    1.13  apply (case_tac "s=UU",clarsimp)