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