/[mojave]/metaprl/theories/itt/itt_set.ml
ViewVC logotype

Diff of /metaprl/theories/itt/itt_set.ml

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

revision 3590 by nogin, Tue Jul 10 00:11:03 2001 UTC revision 3591 by nogin, Sun Apr 28 19:51:58 2002 UTC
# Line 111  Line 111 
111   * DISPLAY FORMS                                                        *   * DISPLAY FORMS                                                        *
112   ************************************************************************)   ************************************************************************)
113    
114  dform set_df1 : {x:'A | 'B} =  dform set_df1 : {x:'A | 'B} = math_set {'x; 'A; 'B}
    pushm[3] `"{ " bvar{'x} `":" slot{'A} `" | " slot{'B} `"}" popm  
115    
116  (************************************************************************  (************************************************************************
117   * RULES                                                                *   * RULES                                                                *

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

  ViewVC Help
Powered by ViewVC 1.1.26