equal
deleted
inserted
replaced
75 |
75 |
76 section "stream_when"; |
76 section "stream_when"; |
77 |
77 |
78 qed_goal "stream_when_strictf" thy "stream_when`UU`s=UU" (fn _ => [ |
78 qed_goal "stream_when_strictf" thy "stream_when`UU`s=UU" (fn _ => [ |
79 stream_case_tac "s" 1, |
79 stream_case_tac "s" 1, |
80 ALLGOALS(asm_simp_tac (HOL_ss addsimps strict_fapp1::stream.when_rews)) |
80 ALLGOALS(asm_simp_tac (HOL_ss addsimps strict_Rep_CFun1::stream.when_rews)) |
81 ]); |
81 ]); |
82 |
82 |
83 |
83 |
84 (* ----------------------------------------------------------------------- *) |
84 (* ----------------------------------------------------------------------- *) |
85 (* theorems about ft and rt *) |
85 (* theorems about ft and rt *) |