Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-27 21:52:11 -0700 (Sun, 27 Jul 2003)
Revision: 4778
Log message:
Gave jprover access to all assumptions (as opposed - to a random subset,
as we had it before). This makes things a lot slower, but also a lot
more consistent.
| Changes | Path |
| +3 -3 | metaprl/support/tactics/top_tacticals.ml |
| +9186 -9896 | metaprl/theories/czf/czf_itt_equiv.prla |
| +72 -83 | metaprl/theories/itt/itt_logic.ml |
| +1 -0 | metaprl/theories/itt/itt_logic.mli |