| changeset 5078 | 7b5ea59c0275 |
| parent 5069 | 3ea049f7979d |
| child 5143 | b94cd208f073 |
--- a/src/HOL/ex/Primrec.ML Wed Jun 24 13:59:45 1998 +0200 +++ b/src/HOL/ex/Primrec.ML Thu Jun 25 13:57:34 1998 +0200 @@ -128,7 +128,7 @@ val lemma = result(); Goal "!!i j k. i<j ==> ack(i,k) < ack(j,k)"; -by (etac less_natE 1); +by (dtac less_eq_Suc_add 1); by (blast_tac (claset() addSIs [lemma]) 1); qed "ack_less_mono1";