/[mojave]/metaprl/theories/czf/czf_itt_isect.ml
ViewVC logotype

Diff of /metaprl/theories/czf/czf_itt_isect.ml

Parent Directory Parent Directory | Revision Log Revision Log | View Patch Patch

revision 3583 by nogin, Wed Jun 20 13:56:53 2001 UTC revision 3584 by nogin, Thu Apr 25 15:28:40 2002 UTC
# Line 176  Line 176 
176  (*!  (*!
177   * @begin[doc]   * @begin[doc]
178   * The elimination form for the general isect $@mem{x; @isect{s}}$ performs   * The elimination form for the general isect $@mem{x; @isect{s}}$ performs
179   * instantiation of of the assumption on a particular set $@mem{z; 's}$.   * instantiation of the assumption on a particular set $@mem{z; 's}$.
180   * @end[doc]   * @end[doc]
181   *)   *)
182  interactive isect_member_elim {| elim [] |} 'H 'J 'z :  interactive isect_member_elim {| elim [] |} 'H 'J 'z :

Legend:
Removed from v.3583  
changed lines
  Added in v.3584

  ViewVC Help
Powered by ViewVC 1.1.26