| changeset 11868 | 56db9f3a6b3e |
| parent 11701 | 3d51fbf81c17 |
| child 13797 | baefae13ad37 |
| 11867:76401b2ee871 | 11868:56db9f3a6b3e |
|---|---|
36 by Safe_tac; |
36 by Safe_tac; |
37 by (auto_tac (claset() addSIs [sum_ext], simpset())); |
37 by (auto_tac (claset() addSIs [sum_ext], simpset())); |
38 qed_spec_mp "sumj_ext"; |
38 qed_spec_mp "sumj_ext"; |
39 |
39 |
40 |
40 |
41 Goal "(ALL i. i<I --> c s i = Numeral0) --> sum I s = Numeral0"; |
41 Goal "(ALL i. i<I --> c s i = 0) --> sum I s = 0"; |
42 by (induct_tac "I" 1); |
42 by (induct_tac "I" 1); |
43 by Auto_tac; |
43 by Auto_tac; |
44 qed "sum0"; |
44 qed "sum0"; |
45 |
45 |
46 |
46 |