| changeset 2496 | 40efb87985b5 |
| parent 2493 | bdeb5024353a |
| child 2637 | e9b203f854ae |
--- a/src/ZF/Epsilon.ML Wed Jan 08 15:17:25 1997 +0100 +++ b/src/ZF/Epsilon.ML Thu Jan 09 10:20:03 1997 +0100 @@ -228,7 +228,7 @@ goal Epsilon.thy "rank(0) = 0"; by (rtac (rank RS trans) 1); -by (fast_tac (!claset addSIs [equalityI]) 1); +by (Fast_tac 1); qed "rank_0"; goal Epsilon.thy "rank(succ(x)) = succ(rank(x))";