changeset 48 | 21291189b51e |
parent 0 | 7949f97df77a |
--- a/ex/term.thy Thu Feb 24 14:45:57 1994 +0100 +++ b/ex/term.thy Wed Mar 02 12:26:55 1994 +0100 @@ -32,7 +32,7 @@ Rep_TList_def "Rep_TList == Rep_map(Rep_Term)" Abs_TList_def "Abs_TList == Abs_map(Abs_Term)" (*defining the abstract constants*) - App_def "App(a,ts) == Abs_Term(Leaf(a) . Rep_TList(ts))" + App_def "App(a,ts) == Abs_Term(Leaf(a) $ Rep_TList(ts))" (*list recursion*) Term_rec_def "Term_rec(M,d) == wfrec(trancl(pred_Sexp), M, \