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

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

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

revision 3583 by jyh, Sun Sep 10 18:26:37 2000 UTC revision 3584 by nogin, Thu Apr 25 15:28:40 2002 UTC
# Line 116  Line 116 
116   * of a @misspelled{forall}/exists formula $@dall{x; s_1; @sexists{s_2; P[x; y]}}$,   * of a @misspelled{forall}/exists formula $@dall{x; s_1; @sexists{s_2; P[x; y]}}$,
117   * there is a set $s_3$ that contains the collection of sets that   * there is a set $s_3$ that contains the collection of sets that
118   * were chosen by the existential.  The reason that the collection is   * were chosen by the existential.  The reason that the collection is
119   * not defined as a set constructor is the the proof of the @misspelled{forall}/exists   * not defined as a set constructor is that the proof of the @misspelled{forall}/exists
120   * formula is part of the construction.  If the set $s_1$ has canonical   * formula is part of the construction.  If the set $s_1$ has canonical
121   * for $s_1 = @collect{x; T; f[x]}$, the proof provides a witness   * for $s_1 = @collect{x; T; f[x]}$, the proof provides a witness
122   * that inhabits the function space $T @rightarrow @set$.  The canonical   * that inhabits the function space $T @rightarrow @set$.  The canonical

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

  ViewVC Help
Powered by ViewVC 1.1.26