equal
deleted
inserted
replaced
191 by (list.induct_tac "xs" 1); |
191 by (list.induct_tac "xs" 1); |
192 by (ALLGOALS Asm_simp_tac); |
192 by (ALLGOALS Asm_simp_tac); |
193 qed "drop_0"; |
193 qed "drop_0"; |
194 |
194 |
195 goal thy "drop (Suc n) (x#xs) = drop n xs"; |
195 goal thy "drop (Suc n) (x#xs) = drop n xs"; |
196 by(Simp_tac 1); |
196 by (Simp_tac 1); |
197 qed "drop_Suc_Cons"; |
197 qed "drop_Suc_Cons"; |
198 |
198 |
199 Delsimps [drop_Cons]; |
199 Delsimps [drop_Cons]; |
200 Addsimps [drop_0,drop_Suc_Cons]; |
200 Addsimps [drop_0,drop_Suc_Cons]; |
201 |
201 |
205 by (list.induct_tac "xs" 1); |
205 by (list.induct_tac "xs" 1); |
206 by (ALLGOALS Asm_simp_tac); |
206 by (ALLGOALS Asm_simp_tac); |
207 qed "take_0"; |
207 qed "take_0"; |
208 |
208 |
209 goal thy "take (Suc n) (x#xs) = x # take n xs"; |
209 goal thy "take (Suc n) (x#xs) = x # take n xs"; |
210 by(Simp_tac 1); |
210 by (Simp_tac 1); |
211 qed "take_Suc_Cons"; |
211 qed "take_Suc_Cons"; |
212 |
212 |
213 Delsimps [take_Cons]; |
213 Delsimps [take_Cons]; |
214 Addsimps [take_0,take_Suc_Cons]; |
214 Addsimps [take_0,take_Suc_Cons]; |
215 |
215 |