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 */