src/Tools/8bit/c-sources/isa2latex/conv-tables.h

Put in minimal simpset to avoid excessive simplification,
just as in revision 1.9 of HOL/indrule.ML

/*
 * translation table for the low-8-bit ascii codes
 * translation takes place only if destCode is TO_LaTeX
 *
 * the row number + START_LOW_TABLE -1 is the ascii code !!
 */

/* do not edit the lines between BEGIN_OF_LOW_TABLE and END_OF_LOW_TABLE  */
/* these lines are automatically generated by gen-isa2latex               */

/* BEGIN_OF_LOW_TABLE */
char *translationTableLow[END_LOW_TABLE - START_LOW_TABLE + 1] = {
   "\\ ",
   "!",
   "\x22{}",
   "\\#",
   "\\$",
   "\\%",
   "\\mbox{$\\&$}",
   "'",
   "(",
   ")",
   "\\mbox{$*$}",
   "\\mbox{$+$}",
   ",",
   "\\mbox{$-$}",
   ".",
   "/",
   "0",
   "1",
   "2",
   "3",
   "4",
   "5",
   "6",
   "7",
   "8",
   "9",
   ":",
   ";",
   "\\mbox{$<$}",
   "\\mbox{$=$}",
   "\\mbox{$>$}",
   "?",
   "@",
   "A",
   "B",
   "C",
   "D",
   "E",
   "F",
   "G",
   "H",
   "I",
   "J",
   "K",
   "L",
   "M",
   "N",
   "O",
   "P",
   "Q",
   "R",
   "S",
   "T",
   "U",
   "V",
   "W",
   "X",
   "Y",
   "Z",
   "\\mbox{$[$}",
   "\\mbox{$\\backslash$}",
   "\\mbox{$]$}",
   "\\^{}",
   "\\_",
   "`",
   "a",
   "b",
   "c",
   "d",
   "e",
   "f",
   "g",
   "h",
   "i",
   "j",
   "k",
   "l",
   "m",
   "n",
   "o",
   "p",
   "q",
   "r",
   "s",
   "t",
   "u",
   "v",
   "w",
   "x",
   "y",
   "z",
   "\\{",
   "\\mbox{$|$}",
   "\\}",
   "\\~{}"
};
/* END_OF_LOW_TABLE */


/*
 * conversion table for Hi-8-bit table
 *
 * the row number + START_HIGH_TABLE -1 is the ascii code !!
 * 
 * first  column is used if destCode is TO_7bit
 * second column is used if destCode is TO_LaTeX
 */

/* do not edit the lines between BEGIN_OF_HI_TABLE and END_OF_HI_TABLE  */
/* these lines are automatically generated by gen-isa2latex             */

/* BEGIN_OF_HI_TABLE */
char *translationTableHi[END_HI_TABLE - START_HI_TABLE + 1][2] = {
   {"\\Gamma"      ,"\\mbox{$\\Gamma$}"},
   {"\\Delta"      ,"\\mbox{$\\Delta$}"},
   {"\\Theta"      ,"\\mbox{$\\Theta$}"},
   {"LAM"          ,"\\mbox{$\\Lambda$}"},
   {"\\Pi"         ,"\\mbox{$\\Pi$}"},
   {"\\Sigma"      ,"\\mbox{$\\Sigma$}"},
   {"\\Phi"        ,"\\mbox{$\\Phi$}"},
   {"\\Psi"        ,"\\mbox{$\\Psi$}"},
   {"\\Omega"      ,"\\mbox{$\\Omega$}"},
   {"'a"           ,"\\mbox{$\\alpha$}"},
   {"'b"           ,"\\mbox{$\\beta$}"},
   {"'c"           ,"\\mbox{$\\gamma$}"},
   {"\\delta"      ,"\\mbox{$\\delta$}"},
   {"\\varepsilon" ,"\\mbox{$\\varepsilon$}"},
   {"\\zeta"       ,"\\mbox{$\\zeta$}"},
   {"\\eta"        ,"\\mbox{$\\eta$}"},
   {"\\vartheta"   ,"\\mbox{$\\vartheta$}"},
   {"\\kappa"      ,"\\mbox{$\\kappa$}"},
   {"%"            ,"\\mbox{$\\lambda$}"},
   {"\\mu"         ,"\\mbox{$\\mu$}"},
   {"\\nu"         ,"\\mbox{$\\nu$}"},
   {"\\xi"         ,"\\mbox{$\\xi$}"},
   {"\\pi"         ,"\\mbox{$\\pi$}"},
   {"'r"           ,"\\mbox{$\\rho$}"},
   {"'s"           ,"\\mbox{$\\sigma$}"},
   {"'t"           ,"\\mbox{$\\tau$}"},
   {"\\varphi"     ,"\\mbox{$\\varphi$}"},
   {"\\chi"        ,"\\mbox{$\\chi$}"},
   {"\\psi"        ,"\\mbox{$\\psi$}"},
   {"\\omega"      ,"\\mbox{$\\omega$}"},
   {"~"            ,"\\mbox{$\\neg$}"},
   {"&"            ,"\\mbox{$\\wedge$}"},
   {"|"            ,"\\mbox{$\\vee$}"},
   {"!"            ,"\\mbox{$\\forall$}"},
   {"?"            ,"\\mbox{$\\exists$}"},
   {"!!"           ,"\\mbox{$\\bigwedge$}"},
   {"\\lceil"      ,"\\mbox{$\\lceil$}"},
   {"\\rceil"      ,"\\mbox{$\\rceil$}"},
   {"\\lfloor"     ,"\\mbox{$\\lfloor$}"},
   {"\\rfloor"     ,"\\mbox{$\\rfloor$}"},
   {"(|"           ,"\\mbox{$(\\!|$}"},
   {"|)"           ,"\\mbox{$|\\!)$}"},
   {"[|"           ,"\\mbox{$[\\![$}"},
   {"|]"           ,"\\mbox{$]\\!]$}"},
   {"\\emptyset"   ,"\\mbox{$\\emptyset$}"},
   {":"            ,"\\mbox{$\\in$}"},
   {"\\subseteq"   ,"\\mbox{$\\subseteq$}"},
   {"Int"          ,"\\mbox{$\\cap$}"},
   {"Un"           ,"\\mbox{$\\cup$}"},
   {"Inter"        ,"\\mbox{$\\bigcap$}"},
   {"Union"        ,"\\mbox{$\\bigcup$}"},
   {"\\sqcap"      ,"\\mbox{$\\sqcap$}"},
   {"\\sqcup"      ,"\\mbox{$\\sqcup$}"},
   {"glb"          ,"\\mbox{$\\overline{|\\,\\,|}$}"},
   {"lub"          ,"\\mbox{$\\bigsqcup$}"},
   {"UU"           ,"\\mbox{$\\perp$}"},
   {"==="          ,"\\mbox{$\\doteq$}"},
   {"=="           ,"\\mbox{$\\equiv$}"},
   {"~="           ,"\\mbox{$\\not=$}"},
   {"\\sqsubset"   ,"\\mbox{$\\sqsubset$}"},
   {"<<"           ,"\\mbox{$\\sqsubseteq$}"},
   {"\\prec"       ,"\\mbox{$\\prec$}"},
   {"\\preceq"     ,"\\mbox{$\\preceq$}"},
   {"\\succ"       ,"\\mbox{$\\succ$}"},
   {"\\succeq"     ,"\\mbox{$\\succeq$}"},
   {"\\sim"        ,"\\mbox{$\\sim$}"},
   {"\\simeq"      ,"\\mbox{$\\simeq$}"},
   {"\\le"         ,"\\mbox{$\\le$}"},
   {"\\ge"         ,"\\mbox{$\\ge$}"},
   {"<-"           ,"\\mbox{$\\leftarrow$}"},
   {"-"            ,"\\mbox{$-$}"},
   {"->"           ,"\\mbox{$\\rightarrow$}"},
   {"<="           ,"\\mbox{$\\Leftarrow$}"},
   {"="            ,"\\mbox{$=$}"},
   {"=>"           ,"\\mbox{$\\Rightarrow$}"},
   {"->>"          ,"\\mbox{$\\twoheadrightarrow$}"},
   {"\\mapsto"     ,"\\mbox{$\\mapsto$}"},
   {"\\leadsto"    ,"\\mbox{$\\leadsto$}"},
   {"\\uparrow"    ,"\\mbox{$\\uparrow$}"},
   {"\\downarrow"  ,"\\mbox{$\\downarrow$}"},
   {"~:"           ,"\\mbox{$\\notin$}"},
   {"*"            ,"\\mbox{$\\times$}"},
   {"++"           ,"\\mbox{$\\oplus$}"},
   {"\\ominus"     ,"\\mbox{$\\ominus$}"},
   {"**"           ,"\\mbox{$\\otimes$}"},
   {"\\oslash"     ,"\\mbox{$\\oslash$}"},
   {"\\natural"    ,"\\mbox{$\\natural$}"},
   {"\\infty"      ,"\\mbox{$\\infty$}"},
   {"\\Box"        ,"\\mbox{$\\Box$}"},
   {"\\Diamond"    ,"\\mbox{$\\Diamond$}"},
   {"\\circ"       ,"\\mbox{$\\circ$}"},
   {"\\bullet"     ,"\\mbox{$\\bullet$}"},
   {"||"           ,"\\mbox{$\\parallel$}"},
   {"\\tick"       ,"\\mbox{$\\surd$}"},
   {"\\filter"     ,"\\mbox{\\copyright}"}
};
/* END_OF_HI_TABLE */


/*
 * conversion table for long ascii and 8bit sequences scanned by lexer
 * 
 * first  column is used if destCode is TO_7bit
 * second column is used if destCode is TO_LaTeX
 *
 * Row - 1 is the code (longCode) used by the lexer
 */      

/* do not edit the lines between BEGIN_OF_SEQ_TABLE and END_OF_SEQ_TABLE  */
/* these lines are automatically generated by gen-isa2latex               */

/* BEGIN_OF_SEQ_TABLE */
char *translationTableSeq[SEQ_TABLE][2] = {
   {"==>"                        ,"\\mbox{$\\Longrightarrow$}"},
   {"-->"                        ,"\\mbox{$\\longrightarrow$}"},
   {"?!"                         ,"\\mbox{$\\exists$}!"},
   {"ALL"                        ,"\\mbox{$\\forall$}"},
   {"EX"                         ,"\\mbox{$\\exists$}"},
   {"<|"                         ,"\\mbox{$<\\!\\mid$}"},
   {"<<|"                        ,"\\mbox{$\\ll\\!\\mid$}"},
   {"<=="                        ,"\\mbox{$\\Longleftarrow$}"},
   {"<=>"                        ,"\\mbox{$\\Leftrightarrow$}"},
   {"<--"                        ,"\\mbox{$\\longleftarrow$}"},
   {"<->"                        ,"\\mbox{$\\leftrightarrow$}"}
};
/* END_OF_SEQ_TABLE */