| changeset 5618 | 721671c68324 |
| parent 5137 | 60205b0de9b9 |
| child 9491 | 1a36151ee2fc |
--- a/src/ZF/ex/Acc.ML Wed Oct 07 10:30:47 1998 +0200 +++ b/src/ZF/ex/Acc.ML Wed Oct 07 10:31:07 1998 +0200 @@ -17,7 +17,7 @@ (*The intended introduction rule*) val prems = goal Acc.thy "[| !!b. <b,a>:r ==> b: acc(r); a: field(r) |] ==> a: acc(r)"; -by (fast_tac (claset() addIs (prems@acc.intrs)) 1); +by (fast_tac (claset() addIs prems@acc.intrs) 1); qed "accI"; Goal "[| b: acc(r); <a,b>: r |] ==> a: acc(r)";