| changeset 11701 | 3d51fbf81c17 |
| parent 11194 | ea13ff5a26d1 |
| child 11868 | 56db9f3a6b3e |
--- a/src/HOL/UNITY/Comp/Counterc.ML Fri Oct 05 21:50:37 2001 +0200 +++ b/src/HOL/UNITY/Comp/Counterc.ML Fri Oct 05 21:52:39 2001 +0200 @@ -38,7 +38,7 @@ qed_spec_mp "sumj_ext"; -Goal "(ALL i. i<I --> c s i = #0) --> sum I s = #0"; +Goal "(ALL i. i<I --> c s i = Numeral0) --> sum I s = Numeral0"; by (induct_tac "I" 1); by Auto_tac; qed "sum0";