src/Pure/Thy/latex.ML
2000-05-24 wenzelm 2000-05-24 proper token_translation for latex mode;
2000-05-21 wenzelm 2000-05-21 replaced {{ }} by { };
2000-05-05 wenzelm 2000-05-05 GPLed;
2000-04-03 wenzelm 2000-04-03 support markup environments;
2000-03-17 wenzelm 2000-03-17 old_symbol_source: include header;
2000-03-15 wenzelm 2000-03-15 tuned comments; renamed isabelle env; proper symbol output for "latex" mode;
2000-02-04 wenzelm 2000-02-04 added old_symbol_source; tuned;
2000-01-10 wenzelm 2000-01-10 isabellesimple: avoid paragraph;
1999-10-29 wenzelm 1999-10-29 \isasymbol renamed to \isasym;
1999-10-21 wenzelm 1999-10-21 output \isasymbols;
1999-10-13 wenzelm 1999-10-13 markup / varbatim: comment out (%) newline char;
1999-10-08 wenzelm 1999-10-08 improved presentation;
1999-10-07 wenzelm 1999-10-07 verbatim markup tokens;
1999-10-06 wenzelm 1999-10-06 improved presentation;
1999-10-06 wenzelm 1999-10-06 accomodate markup commands;
1999-10-05 wenzelm 1999-10-05 strip_blanks;
1999-10-05 wenzelm 1999-10-05 Simple LaTeX presentation primitives (based on outer lexical syntax).