Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/MacroHints
changeset 137 ad5414f5540c
parent 107 b4a8dabc7313 
--- 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
isabelle