| changeset 6711 | d45359e7dcbf |
| parent 6536 | 281d44905cab |
| child 7403 | c318acb88251 |
--- a/src/HOL/UNITY/Token.ML Mon May 24 15:49:24 1999 +0200 +++ b/src/HOL/UNITY/Token.ML Mon May 24 15:49:44 1999 +0200 @@ -108,7 +108,7 @@ Goal "j<N ==> F : ({s. token s < N} Int H j) leadsTo (E j)"; by (rtac (leadsTo_cancel1 RS leadsTo_Un_duplicate) 1); by (rtac TR6 2); -by (rtac leadsTo_weaken_R 1); +by (rtac leadsTo_weaken 1); by (rtac ([leadsTo_j, TR3] MRS psp) 1); by (ALLGOALS Blast_tac); qed "token_progress";