--- 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;
-