src/HOL/UNITY/Comp/Counter.ML

               simpset() addsimps [p2_p3_lemma1 RS sym]));
 qed "p2_p3";
 
 (* 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'";
 val sum0_lemma =  (sum_0' RS mp) RS sym;