| changeset 3840 | e0baea4d485a |
| parent 1478 | 2b8c2a7547ab |
| child 11319 | 8b84ee2cc79c |
--- a/src/ZF/Resid/Residuals.thy Fri Oct 10 18:17:17 1997 +0200 +++ b/src/ZF/Resid/Residuals.thy Fri Oct 10 18:23:31 1997 +0200 @@ -31,6 +31,6 @@ type_intrs "[subst_type]@nat_typechecks@redexes.intrs@bool_typechecks" rules - res_func_def "u |> v == THE w.residuals(u,v,w)" + res_func_def "u |> v == THE w. residuals(u,v,w)" end