doc-src/MacroHints

Tidied some proofs, maybe using less_SucE

+
−
+
−Hints
+
−=====
+
−
+
−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
+
−  (elaborate on this in last sect of 'Defining Logics' (?));
+
−
+
−- 'Variable --> Constant' possible during rewriting;
+
−
+
−- 'trivial definitions' via macros (e.g. "x ~= y" == "~ (x = y)");
+
−
+
−- patterns matching any remaining arguments are not possible (i.e. what would
+
−  be (f x y . zs) in LISP); e.g. HOL's @ (supposing it implemented via macros
+
−  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: 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
+
−  applications will be introduced;
+
−