Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-03-21 01:49:42 -0800 (Fri, 21 Mar 2003)
Revision: 4204
Log message:

      Added a set membership elimination rule.
      
      Alexei, what's your take on membership elimination rules in general - how should
      we manage those? Proving a separate mem. elim for each elim seems somewhat silly...
      Alos, what's a good place for this rule? In can not go into itt_set since it requires
      itt_logic, but itt_struct2 does not seem right either.
      

Changes	Path
+9 -0	metaprl/theories/itt/itt_struct2.ml
+4285 -4430	metaprl/theories/itt/itt_struct2.prla