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

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

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

revision 3590 by xiny, Tue Apr 9 05:57:26 2002 UTC revision 3591 by nogin, Sun Apr 28 19:51:58 2002 UTC
# Line 32  Line 32 
32  let fold_inv_image = makeFoldC << inv_image{'s; x. 'a['x]; 't} >> unfold_inv_image  let fold_inv_image = makeFoldC << inv_image{'s; x. 'a['x]; 't} >> unfold_inv_image
33    
34  dform inv_image_df : parens :: except_mode[src] :: inv_image{'s; x. 'a; 't} =  dform inv_image_df : parens :: except_mode[src] :: inv_image{'s; x. 'a; 't} =
35     pushm[0] `"{" slot{'x} " " Nuprl_font!member `"s " slot{'s} `" | " slot{'a} " " Nuprl_font!member `"s " slot{'t} `"}" popm     pushm[0] `"{" slot{'x} " " Nuprl_font!member `"s " slot{'s} mid slot{'a} " " Nuprl_font!member `"s " slot{'t} `"}" popm
36    
37  (*  (*
38   * Axioms for inverse image.   * Axioms for inverse image.

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

  ViewVC Help
Powered by ViewVC 1.1.26