author lcp
Fri, 07 Apr 1995 10:12:01 +0200
changeset 1022 c4921e635bf7
parent 137 ad5414f5540c
permissions -rw-r--r--
Local version of (original) hypsubst: needs no simplifier


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

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