Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-05 14:18:03 -0700 (Wed, 05 Apr 2006)
Revision: 9024
Log message:

      More progress on elimination tactics. They are now mostly complete, except for
      the "big step elimination" rule, where we get the following unproved subgoals:
      
      - A few wf subgoals for the "bindn {..sequent_bterm{0}}" in
        pnm_core_judgments. Hopefully they will go away at the same time we fix them
        for the intro rules.
      
      - The subgoals corresponding to the "subtheory" cases. Currently the
        assumptions we generate for subtheories in these "big step elimination"
        rules are simply incorrect and we need to figure out what to do about it. It
        seems that the best thing to do would be to fully expalnd the subtheories
        (so that we get cases for all the rules, including the ones from
        subtheories), but this approach might have its own downsides.