diff -r a9015b16a0e5 -r ad5414f5540c doc-src/MacroHints --- a/doc-src/MacroHints Mon Nov 22 11:28:25 1993 +0100 +++ b/doc-src/MacroHints Mon Nov 22 12:08:45 1993 +0100 @@ -3,11 +3,13 @@ ===== 22-Oct-1993 MMW +20-Nov-1993 MMW Some things notable, but not (yet?) covered by the manual. -- constants of result type prop should always supply concrete syntax; +- constants of result type prop should always supply concrete syntax + (elaborate on this in last sect of 'Defining Logics' (?)); - 'Variable --> Constant' possible during rewriting; @@ -18,7 +20,8 @@ which it is *not*): "@x. P" == "Eps(%x. P)", now the print rule doesn't match things like Eps(%x. P, a, b, c); -- alpha: the precise manner in which bounds are renamed for printing; +- alpha: document the precise manner in which bounds are renamed for + printing; - parsing: applications like f(x)(y)(z) are not parse-ast-translated into (f x y z); this may cause some problems, when the notation "f x y z" for