diff -r 80ebd1a213fd -r b239c202c91f doc-src/MacroHints
--- a/doc-src/MacroHints	Fri Nov 29 18:03:21 1996 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-
-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;
-