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

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