changeset 114 | b7f57e0ab47c |
parent 72 | 30e80f028c57 |
child 127 | d9527f97246e |
--- a/ex/Term.thy Thu Aug 18 12:42:19 1994 +0200 +++ b/ex/Term.thy Thu Aug 18 12:48:03 1994 +0200 @@ -40,7 +40,7 @@ (*list recursion*) Term_rec_def "Term_rec(M,d) == wfrec(trancl(pred_Sexp), M, \ -\ %M g. Split(M, %x y. d(x,y, Abs_map(g,y))))" +\ Split(%x y g. d(x,y, Abs_map(g,y))))" term_rec_def "term_rec(t,d) == \