Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-01-05 21:14:32 -0800 (Mon, 05 Jan 2004)
Revision: 5226
Log message:

      One of the rules already had a proof and does not need to be an axiom.
      

Changes	Path
+25 -30	metaprl/theories/czf/czf_itt_equiv.ml