Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-02-13 00:31:35 -0800 (Fri, 13 Feb 2004)
Revision: 5371
Log message:
Added an nth_hyp resource. Any axiom (e.g. assumption-free rule) of the form
<H>; x: ...; <J[x]> >- ...
can now be annotated with {| nth_hyp |}. The corresponding tactic is
Auto_tactic.nthHypT (the old limited Itt_struct.nthHypT went away),
which is also included in trivialT and autoT.