Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-29 23:41:33 -0700 (Tue, 29 Apr 2003)
Revision: 4521
Log message:
This is an attempt to give sequents and variables more consistent look:
- I got rid of math_sequent, so now the sequents in documentation
have to be entered using << >> term quotations.
- The "H" -> Gamma translation would now be done on contexts that have a number
after a name
- The "H" -> Gamma translation would now also be done on context arguments to a rule
- The translation of variable suffixes into subscripts will now also be
done in html mode, not just tex mode.
- The translation of variable suffixes into subscripts (tex, html modes) should
now work correctly in most binding positions.
Note: to make this work I had to remove aggressive "debindification" of hypothesis
from the Term_gen