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