| changeset 13454 | 01e2496dee05 |
| parent 11655 | 923e4d0d36d5 |
| child 14171 | 0cab06e3bbd0 |
--- a/src/HOLCF/FOCUS/Buffer.ML Mon Aug 05 14:30:06 2002 +0200 +++ b/src/HOLCF/FOCUS/Buffer.ML Mon Aug 05 14:32:56 2002 +0200 @@ -160,7 +160,7 @@ Goal "\\<forall>s f ff. f\\<in>BufEq \\<longrightarrow> ff\\<in>BufEq \\<longrightarrow> \ \ s\\<in>BufAC_Asm \\<longrightarrow> stream_take n\\<cdot>(f\\<cdot>s) = stream_take n\\<cdot>(ff\\<cdot>s)"; -by (nat_ind_tac "n" 1); +by (induct_tac "n" 1); by (Simp_tac 1); by (strip_tac 1); by (dtac (BufAC_Asm_unfold RS iffD1) 1);