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 |