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

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

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

revision 3583 by nogin, Sun Jun 24 10:25:49 2001 UTC revision 3584 by nogin, Thu Apr 25 15:28:40 2002 UTC
# Line 8  Line 8 
8   * Contrary to the name, the subset collection is @emph{not} a   * Contrary to the name, the subset collection is @emph{not} a
9   * power set, but it has some similarities.  The subset collection   * power set, but it has some similarities.  The subset collection
10   * constructor has the form $@power{s_1; s_2}$, where $s_1$ and   * constructor has the form $@power{s_1; s_2}$, where $s_1$ and
11   * $s_2$ are sets.  If the the canonical forms are $s_1 = @collect{x_1; T_1; f_1[x_1]}$   * $s_2$ are sets.  If the canonical forms are $s_1 = @collect{x_1; T_1; f_1[x_1]}$
12   * and $s_2 = @collect{x_2; T_2; f_2[x_2]}$, the elements of the   * and $s_2 = @collect{x_2; T_2; f_2[x_2]}$, the elements of the
13   * power set are the subsets of $s_2$ that are defined by   * power set are the subsets of $s_2$ that are defined by
14   * the images of the computable functions in the space $@fun{T_1; T_2}$.   * the images of the computable functions in the space $@fun{T_1; T_2}$.

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

  ViewVC Help
Powered by ViewVC 1.1.26