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