103

1 


2 
Hints


3 
=====


4 

107

5 
22Oct1993 MMW

137

6 
20Nov1993 MMW

107

7 


8 
Some things notable, but not (yet?) covered by the manual.

103

9 


10 

137

11 
 constants of result type prop should always supply concrete syntax


12 
(elaborate on this in last sect of 'Defining Logics' (?));

103

13 

107

14 
 'Variable > Constant' possible during rewriting;

103

15 

107

16 
 'trivial definitions' via macros (e.g. "x ~= y" == "~ (x = y)");

103

17 

107

18 
 patterns matching any remaining arguments are not possible (i.e. what would


19 
be (f x y . zs) in LISP); e.g. HOL's @ (supposing it implemented via macros


20 
which it is *not*): "@x. P" == "Eps(%x. P)", now the print rule doesn't


21 
match things like Eps(%x. P, a, b, c);

103

22 

137

23 
 alpha: document the precise manner in which bounds are renamed for


24 
printing;

103

25 

107

26 
 parsing: applications like f(x)(y)(z) are not parseasttranslated into


27 
(f x y z); this may cause some problems, when the notation "f x y z" for


28 
applications will be introduced;

103

29 
