| changeset 7086 | f9aa63a5a8b6 |
| parent 7075 | 5ba8d1e42ca6 |
| child 7127 | 48e235179ffb |
--- a/src/HOL/Integ/NatBin.ML Mon Jul 26 16:30:50 1999 +0200 +++ b/src/HOL/Integ/NatBin.ML Mon Jul 26 16:32:23 1999 +0200 @@ -44,7 +44,7 @@ (** Successor **) Goal "(#0::int) <= z ==> Suc (nat z) = nat (#1 + z)"; -br sym 1; +by (rtac sym 1); by (asm_simp_tac (simpset() addsimps [nat_eq_iff]) 1); qed "Suc_nat_eq_nat_zadd1";