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

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

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

revision 3590 by xiny, Tue Apr 9 05:57:54 2002 UTC revision 3591 by nogin, Sun Apr 28 19:51:58 2002 UTC
# Line 35  Line 35 
35  let resource reduce += << set_bvd{collect{'T; x. 'f['x]}; x. 'a['x]} >>, reduce_set_bvd  let resource reduce += << set_bvd{collect{'T; x. 'f['x]}; x. 'a['x]} >>, reduce_set_bvd
36    
37  dform set_bvd_df : parens :: except_mode[src] :: set_bvd{'s; x. 'a} =  dform set_bvd_df : parens :: except_mode[src] :: set_bvd{'s; x. 'a} =
38     pushm[0] `"{" slot{'a} `" | " slot{'x} " " Nuprl_font!member `"s " slot{'s} `"}" popm     pushm[0] `"{" slot{'a} mid slot{'x} " " Nuprl_font!member `"s " slot{'s} `"}" popm
39    
40  dform setbvd_prop_df : parens :: except_mode[src] :: setbvd_prop{'s; x. 'p} =  dform setbvd_prop_df : parens :: except_mode[src] :: setbvd_prop{'s; x. 'p} =
41     pushm[0] `"{" slot{'x} " " Nuprl_font!member `"s " slot{'s} `" | " slot{'p} `"}" popm     pushm[0] `"{" slot{'x} " " Nuprl_font!member `"s " slot{'s} mid slot{'p} `"}" popm
42    
43  (*  (*
44   * Propertiess for set builder.   * Propertiess for set builder.

Legend:
Removed from v.3590  
changed lines
  Added in v.3591

  ViewVC Help
Powered by ViewVC 1.1.26