| changeset 11868 | 56db9f3a6b3e |
| parent 11701 | 3d51fbf81c17 |
| child 13797 | baefae13ad37 |
--- a/src/HOL/UNITY/Comp/Counterc.ML Mon Oct 22 11:01:30 2001 +0200 +++ b/src/HOL/UNITY/Comp/Counterc.ML Mon Oct 22 11:54:22 2001 +0200 @@ -38,7 +38,7 @@ qed_spec_mp "sumj_ext"; -Goal "(ALL i. i<I --> c s i = Numeral0) --> sum I s = Numeral0"; +Goal "(ALL i. i<I --> c s i = 0) --> sum I s = 0"; by (induct_tac "I" 1); by Auto_tac; qed "sum0";