Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-28 03:12:14 -0800 (Wed, 28 Jan 2004)
Revision: 5302
Log message:
Added a Sequent.all_hyps function that returns a list of all hypothesis in
the goal sequent.
Changes | Path |
+13 -1 | metaprl/tactics/proof/sequent_boot.ml |
+1 -0 | metaprl/tactics/proof/tactic_boot_sig.ml |
+1 -5 | metaprl/theories/itt/itt_logic.ml |
+1 -22 | metaprl/theories/itt/itt_supinf.ml |