| #
21cc9432 |
|
26-Oct-2001 |
Konrad Slind <konrad.slind@gmail.com> |
Preliminary implementation of a set of inference rules for named
hypotheses. Currently incomplete, but would like to extend to
give versions of PROVE_TAC and SIMP_TAC that will use names to determine
which assumptions to use in inference. After that, it might be
fun to implement a slick version of Freek Wiedijk's Mizar Mode.
I'm just sticking this here for backup purposes.
|