changeset 5656 | f8389824189b |
parent 5192 | 704dd3a6d47d |
child 10212 | 33fe2d701ddd |
--- a/src/HOLCF/IOA/NTP/Lemmas.ML Fri Oct 16 17:32:29 1998 +0200 +++ b/src/HOLCF/IOA/NTP/Lemmas.ML Fri Oct 16 17:33:43 1998 +0200 @@ -37,7 +37,6 @@ goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))"; by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1); -by (Blast_tac 1); qed "pred_suc";