| changeset 3842 | b55686a7b22c |
| parent 3268 | 012c43174664 |
| child 5184 | 9b8547a9496a |
--- a/src/HOL/Subst/Subst.thy Fri Oct 10 18:37:49 1997 +0200 +++ b/src/HOL/Subst/Subst.thy Fri Oct 10 19:02:28 1997 +0200 @@ -26,7 +26,7 @@ defs - subst_eq_def "r =$= s == ALL t.t <| r = t <| s" + subst_eq_def "r =$= s == ALL t. t <| r = t <| s" comp_def "al <> bl == alist_rec al bl (%x y xs g. (x,y <| bl)#g)"