| changeset 4833 | 2e53109d4bc8 |
| parent 4532 | 006e5572aca8 |
| child 5192 | 704dd3a6d47d |
--- a/src/HOLCF/IOA/NTP/Lemmas.ML Mon Apr 27 16:46:56 1998 +0200 +++ b/src/HOLCF/IOA/NTP/Lemmas.ML Mon Apr 27 16:47:50 1998 +0200 @@ -36,7 +36,7 @@ (* Arithmetic *) goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))"; -by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [expand_nat_case]) 1); +by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [split_nat_case]) 1); by (Blast_tac 1); qed "pred_suc";