/[mojave]/metaprl/theories/tactic/nuprl_font.ml
ViewVC logotype

Diff of /metaprl/theories/tactic/nuprl_font.ml

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

revision 3590 by nogin, Sun Mar 10 23:29:54 2002 UTC revision 3591 by nogin, Sun Apr 28 19:51:58 2002 UTC
# Line 160  Line 160 
160  declare Leftrightarrow  declare Leftrightarrow
161  declare ulcorner  declare ulcorner
162  declare urcorner  declare urcorner
163    declare mid
164  declare vdash  declare vdash
165  declare integral  declare integral
166  declare cdot  declare cdot
# Line 691  Line 692 
692  dform leftrightarrow_df         : internal :: mode[tex] :: Leftrightarrow            = mathmacro["leftrightarrow"]  dform leftrightarrow_df         : internal :: mode[tex] :: Leftrightarrow            = mathmacro["leftrightarrow"]
693  dform ulcorner_df               : internal :: mode[tex] :: ulcorner                  = mathmacro["ulcorner"]  dform ulcorner_df               : internal :: mode[tex] :: ulcorner                  = mathmacro["ulcorner"]
694  dform urcorner_df               : internal :: mode[tex] :: urcorner                  = mathmacro["urcorner"]  dform urcorner_df               : internal :: mode[tex] :: urcorner                  = mathmacro["urcorner"]
695    dform mid            : internal :: mode[tex] :: mid                       = `"|"
696  dform vdash_df                  : internal :: mode[tex] :: vdash                     = mathmacro["vdash"]  dform vdash_df                  : internal :: mode[tex] :: vdash                     = mathmacro["vdash"]
697  dform integral_df               : internal :: mode[tex] :: integral                  = mathmacro["int"]  dform integral_df               : internal :: mode[tex] :: integral                  = mathmacro["int"]
698  dform cdot_df                   : internal :: mode[tex] :: cdot                      = mathmacro["cdot"]  dform cdot_df                   : internal :: mode[tex] :: cdot                      = mathmacro["cdot"]
# Line 870  Line 872 
872  (*  (*
873   * Source   * Source
874   *)   *)
875    dform mid_df : internal :: except_mode[tex] :: mid = `" | "
876  dform leftarrow_df : internal :: mode[src] :: Leftarrow = `"<="  dform leftarrow_df : internal :: mode[src] :: Leftarrow = `"<="
877  dform leftrightarrow_df : internal :: mode[src] :: Leftrightarrow = `"<=>"  dform leftrightarrow_df : internal :: mode[src] :: Leftrightarrow = `"<=>"
878  dform rightarrow_df : internal :: mode[src] :: Rightarrow = `"=>"  dform rightarrow_df : internal :: mode[src] :: Rightarrow = `"=>"

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

  ViewVC Help
Powered by ViewVC 1.1.26