src/ZF/ex/Primrec.ML
changeset 6163 be8234f37e48
parent 6154 6a00a5baef2b
child 7499 23e090051cb8
     1.1 --- a/src/ZF/ex/Primrec.ML	Fri Jan 29 16:26:12 1999 +0100
     1.2 +++ b/src/ZF/ex/Primrec.ML	Fri Jan 29 17:08:20 1999 +0100
     1.3 @@ -159,7 +159,7 @@
     1.4  \             i#+j < ack(succ(succ(succ(succ(k)))), j)";
     1.5  by (res_inst_tac [("j", "ack(k,j) #+ ack(0,j)")] lt_trans 1);
     1.6  by (rtac (ack_add_bound RS lt_trans2) 2);
     1.7 -br add_lt_mono 1;
     1.8 +by (rtac add_lt_mono 1);
     1.9  by Auto_tac;
    1.10  qed "ack_add_bound2";
    1.11