changeset 1957 | 58b60b558e48 |
parent 1461 | 6bcb44e4d6e5 |
child 2469 | b50b8c0eec01 |
--- a/src/ZF/OrderArith.ML Thu Sep 05 18:30:13 1996 +0200 +++ b/src/ZF/OrderArith.ML Thu Sep 05 18:31:14 1996 +0200 @@ -79,7 +79,7 @@ by (rtac wf_onI2 1); by (subgoal_tac "ALL x:A. Inl(x): Ba" 1); (*Proving the lemma, which is needed twice!*) -by (eres_inst_tac [("V", "y : A + B")] thin_rl 2); +by (thin_tac "y : A + B" 2); by (rtac ballI 2); by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2); by (etac (bspec RS mp) 2);