# HG changeset patch
# User paulson
# Date 1234261509 0
# Node ID e0ab6cf95539c3c60a47761e4d8e8bd817a0205a
# Parent  708c1c7c87ec8930477093d336912cfbc6850b9c
Repaired a proof that did, after all, refer to the theorem nat_induct2.

diff -r 708c1c7c87ec -r e0ab6cf95539 src/HOLCF/ex/Stream.thy
--- a/src/HOLCF/ex/Stream.thy	Tue Feb 10 09:58:58 2009 +0000
+++ b/src/HOLCF/ex/Stream.thy	Tue Feb 10 10:25:09 2009 +0000
@@ -252,7 +252,9 @@
 lemma stream_finite_ind2:
 "[| P UU; !! x. x ~= UU ==> P (x && UU); !! y z s. [| y ~= UU; z ~= UU; P s |] ==> P (y && z && s )|] ==>
                                  !s. P (stream_take n$s)"
-apply (rule nat_induct2 [of _ n],auto)
+apply (rule nat_less_induct [of _ n],auto)
+apply (case_tac n, auto) 
+apply (case_tac nat, auto) 
 apply (case_tac "s=UU",clarsimp)
 apply (drule stream_exhaust_eq [THEN iffD1],clarsimp)
 apply (case_tac "s=UU",clarsimp)