| changeset 10212 | 33fe2d701ddd |
| parent 5656 | f8389824189b |
| child 10215 | 1ead773b365e |
--- a/src/HOLCF/IOA/NTP/Lemmas.ML Thu Oct 12 18:09:06 2000 +0200 +++ b/src/HOLCF/IOA/NTP/Lemmas.ML Thu Oct 12 18:38:23 2000 +0200 @@ -35,7 +35,7 @@ (* Arithmetic *) -goal Arith.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))"; +goal Arithmetic.thy "!!x. 0<x ==> (x-1 = y) = (x = Suc(y))"; by (asm_simp_tac (simpset() addsimps [diff_Suc] addsplits [nat.split]) 1); qed "pred_suc";