changeset 11704 | 3c50a2cd6f00 |
parent 11701 | 3d51fbf81c17 |
child 11868 | 56db9f3a6b3e |
--- a/src/HOL/Integ/int_arith2.ML Fri Oct 05 23:58:52 2001 +0200 +++ b/src/HOL/Integ/int_arith2.ML Sat Oct 06 00:02:46 2001 +0200 @@ -75,7 +75,7 @@ by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); qed "nat_1"; -Goal "nat # 2 = Suc (Suc 0)"; +Goal "nat 2 = Suc (Suc 0)"; by (simp_tac (simpset() addsimps [nat_eq_iff]) 1); qed "nat_2";