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

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

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

revision 3590 by nogin, Thu Apr 25 15:28:40 2002 UTC revision 3591 by nogin, Sun Apr 28 19:51:58 2002 UTC
# Line 435  Line 435 
435     izone `"\\mathrel{\\bf with}" ezone     izone `"\\mathrel{\\bf with}" ezone
436     math_inl{'y}     math_inl{'y}
437     izone `"\\rightarrow " ezone     izone `"\\rightarrow " ezone
438     slot{'a}     slot{'a} `"|" math_inr{'z}
    izone `"\\mathrel{|} " ezone  
    math_inr{'z}  
439     izone `"\\rightarrow " ezone     izone `"\\rightarrow " ezone
440     slot{'b}     slot{'b}
441     izone `"}" ezone     izone `"}" ezone
# Line 524  Line 522 
522   *)   *)
523  dform math_rfun_df1 : mode[tex] :: math_rfun{'f; 'x; 'A; 'B} =  dform math_rfun_df1 : mode[tex] :: math_rfun{'f; 'x; 'A; 'B} =
524     izone `"\\left\\{" ezone     izone `"\\left\\{" ezone
525     'f     'f `"|" 'x
    izone `"\\mathrel{|}" ezone  
    'x  
526     izone `"\\colon " ezone     izone `"\\colon " ezone
527     'A     'A
528     izone `"\\rightarrow " ezone     izone `"\\rightarrow " ezone
# Line 652  Line 648 
648     slot{bvar{'x}} `":" slot{'A} " " rightarrow " " slot{'B}     slot{bvar{'x}} `":" slot{'A} " " rightarrow " " slot{'B}
649    
650  dform fun_df3 : except_mode[tex] :: math_rfun{'f; 'x; 'A; 'B} =  dform fun_df3 : except_mode[tex] :: math_rfun{'f; 'x; 'A; 'B} =
651     "{" " " slot{bvar{'f}} `" | "  math_fun{'x; 'A; 'B} `" }"     "{" " " slot{bvar{'f}} mid math_fun{'x; 'A; 'B} `" }"
652    
653  dform apply_df1 : parens :: "prec"[prec_apply] :: except_mode[tex] :: math_apply{'f; 'a} =  dform apply_df1 : parens :: "prec"[prec_apply] :: except_mode[tex] :: math_apply{'f; 'a} =
654     slot["lt"]{'f} " " slot["le"]{'a}     slot["lt"]{'f} " " slot["le"]{'a}
# Line 849  Line 845 
845   *)   *)
846    
847  dform math_set_df1 : mode[tex] :: math_set{'x; 'A; 'B} =  dform math_set_df1 : mode[tex] :: math_set{'x; 'A; 'B} =
848     izone `"{\\left\\{" ezone     izone `"\\left\\{" ezone
849     slot{'x}     slot{'x}
850     izone `"\\colon " ezone     izone `"\\colon " ezone
851     slot{'A}     slot{'A} `"|" slot{'B}
852     izone `"\\mathrel{|} " ezone     izone `"\\right\\}" ezone
    slot{'B}  
    izone `"\\right\\}}" ezone  
853    
854  dform math_squash_df1 : mode[tex] :: math_squash{'A} =  dform math_squash_df1 : mode[tex] :: math_squash{'A} =
855     izone `"\\sq{" ezone     izone `"\\sq{" ezone
# Line 866  Line 860 
860   * Normal mode   * Normal mode
861   *)   *)
862  dform set_df1 : except_mode[tex] :: math_set{'x; 'A; 'B} =  dform set_df1 : except_mode[tex] :: math_set{'x; 'A; 'B} =
863     pushm[3] `"{ " bvar{'x} `":" slot{'A} `" | " slot{'B} `"}" popm     pushm[3] `"{" bvar{'x} `":" slot{'A} mid slot{'B} `"}" popm
864    
865  dform math_squash_df2 : except_mode[tex] :: math_squash{'A} = "[" 'A "]"  dform math_squash_df2 : except_mode[tex] :: math_squash{'A} = "[" 'A "]"
866    

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

  ViewVC Help
Powered by ViewVC 1.1.26