/[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 3583 by nogin, Tue Jul 10 00:11:03 2001 UTC revision 3584 by nogin, Thu Apr 25 15:28:40 2002 UTC
# Line 523  Line 523 
523   * TeX mode   * TeX mode
524   *)   *)
525  dform math_rfun_df1 : mode[tex] :: math_rfun{'f; 'x; 'A; 'B} =  dform math_rfun_df1 : mode[tex] :: math_rfun{'f; 'x; 'A; 'B} =
526     izone `"{\\left\\{"     izone `"\\left\\{" ezone
527     'f     'f
528     izone `"\\mathrel{|}" ezone     izone `"\\mathrel{|}" ezone
529     'x     'x
# Line 531  Line 531 
531     'A     'A
532     izone `"\\rightarrow " ezone     izone `"\\rightarrow " ezone
533     'B     'B
534     izone `"\\right\\}}" ezone     izone `"\\right\\}" ezone
535    
536  dform math_dfun_df1 : mode[tex] :: math_fun{'x; 'A; 'B} =  dform math_dfun_df1 : mode[tex] :: math_fun{'x; 'A; 'B} =
    izone `"{" ezone  
537     'x     'x
538     izone `"\\colon " ezone     izone `"\\colon " ezone
539     'A     'A
540     izone `"\\rightarrow " ezone     izone `"\\rightarrow " ezone
541     'B     'B
    izone `"}" ezone  
542    
543  dform math_fun_df1 : mode[tex] :: math_fun{'A; 'B} =  dform math_fun_df1 : mode[tex] :: math_fun{'A; 'B} =
    izone `"{" ezone  
544     'A     'A
545     izone `"\\rightarrow " ezone     izone `"\\rightarrow " ezone
546     'B     'B
    izone `"}" ezone  
547    
548  dform math_lambda_df1 : mode[tex] :: math_lambda{'v; 'b} =  dform math_lambda_df1 : mode[tex] :: math_lambda{'v; 'b} =
549     izone `"{\\lambda " ezone     izone `"\\lambda " ezone
550     'v     'v
551     izone `"." ezone     izone `"." ezone
552     'b     'b
    izone `"}" ezone  
553    
554  dform math_lambda_df1 : mode[tex] :: math_lambda =  dform math_lambda_df1 : mode[tex] :: math_lambda =
555     izone `"\\lambda " ezone     izone `"\\lambda " ezone
556    
557  dform math_apply_df1 : mode[tex] :: math_apply{'f; 'a} =  dform math_apply_df1 : mode[tex] :: math_apply{'f; 'a} =
    izone `"{" ezone  
558     'f     'f
559     izone `"\\ " ezone     izone `"\\ " ezone
560     'a     'a
    izone `"}" ezone  
561    
562  dform math_well_founded_df1 : mode[tex] :: math_well_founded{'A; 'x; 'y; 'R} =  dform math_well_founded_df1 : mode[tex] :: math_well_founded{'A; 'x; 'y; 'R} =
563     izone `"{{\\it well\\_founded}(" ezone     izone `"{{\\it well\\_founded}(" ezone

Legend:
Removed from v.3583  
changed lines
  Added in v.3584

  ViewVC Help
Powered by ViewVC 1.1.26