2015-10-17 wenzelm 2015-10-17 more explicit output of list items;
2015-10-17 wenzelm 2015-10-17 tuned;
2015-10-17 wenzelm 2015-10-17 clarified nesting of paragraphs: indentation is taken into account more uniformly; tuned;
2015-10-16 wenzelm 2015-10-16 Markdown support in document text;
2015-10-16 wenzelm 2015-10-16 clarified Antiquote.antiq_reports; Thy_Output.output_text: support for markdown (inactive); eliminared Thy_Output.check_text -- uniform use of Thy_Output.output_text;
2015-10-15 wenzelm 2015-10-15 trim_blanks after read, before eval; clarified Raw_Token: uniform output_text; tuned signature;
2015-10-15 wenzelm 2015-10-15 clarified modules;
2015-10-15 wenzelm 2015-10-15 load markdown.ML into Pure;
2015-10-15 wenzelm 2015-10-15 proper recursive nesting of adjacent lists;
2015-10-15 wenzelm 2015-10-15 tuned;
2015-10-15 wenzelm 2015-10-15 clarified line content: source without marker prefix;
2015-10-15 wenzelm 2015-10-15 more markup;
2015-10-15 wenzelm 2015-10-15 report Markdown document structure;
2015-10-15 wenzelm 2015-10-15 more comments;
2015-10-15 wenzelm 2015-10-15 unused -- avoid confusion in Symbols dockable;
2015-10-15 wenzelm 2015-10-15 proper nesting of adjacent lists;
2015-10-15 wenzelm 2015-10-15 more document structure; tuned signature;
2015-10-14 wenzelm 2015-10-14 more document structure;
2015-10-14 wenzelm 2015-10-14 more document structure;
2015-10-14 wenzelm 2015-10-14 clarified;
2015-10-14 wenzelm 2015-10-14 minimal support for Markdown documents;
2015-10-14 wenzelm 2015-10-14 clarified;
2015-10-14 wenzelm 2015-10-14 more symbols;
2015-10-14 wenzelm 2015-10-14 more symbols;
2015-10-14 wenzelm 2015-10-14 clarified control symbols;
2015-10-14 wenzelm 2015-10-14 added glyphs 0x21e4, 0x21e5, 0x27a7 from DejaVuSansMono;
2015-10-13 wenzelm 2015-10-13 tuned signature (cf. XML.trim_blanks);
2015-10-13 wenzelm 2015-10-13 added split_lines; tuned signature;
2015-10-17 haftmann 2015-10-17 qualify some names stemming from internal bootstrap constructions
2015-10-15 blanchet 2015-10-15 removed too aggressive underscorization
2015-10-13 nipkow 2015-10-13 typo
2015-10-13 nipkow 2015-10-13 prefer undecorated typedef
2015-10-13 nipkow 2015-10-13 even -> evn to avoid clash with global even
2015-10-13 nipkow 2015-10-13 added invar empty
2015-10-13 paulson 2015-10-13 Fixed nonterminating "blast" proof
2015-10-13 paulson 2015-10-13 new material on path_component_sets, inside, outside, etc. And more default simprules
2015-10-13 haftmann 2015-10-13 restored print translation from a1141fb798ff, to prevent a printing misfit observable using "thm divmod_nat_if" in theory "Divides", with a meagure indication in the comment
2015-10-13 haftmann 2015-10-13 prod_case as canonical name for product type eliminator
2015-10-13 haftmann 2015-10-13 emphasized general nature of parameter
2015-10-13 haftmann 2015-10-13 moved lemmas
2015-10-12 wenzelm 2015-10-12 more symbols;
2015-10-12 wenzelm 2015-10-12 redundant due to \parindent 0pt;
2015-10-12 wenzelm 2015-10-12 isabelle update_cartouches;
2015-10-12 wenzelm 2015-10-12 scalable fonts for T1 encoding;
2015-10-12 wenzelm 2015-10-12 proper imports; more symbols; avoid special latex tricks;
2015-10-12 wenzelm 2015-10-12 more symbols;
2015-10-12 wenzelm 2015-10-12 more symbols;
2015-10-12 wenzelm 2015-10-12 more antiquotations;
2015-10-12 wenzelm 2015-10-12 proper message;
2015-10-12 wenzelm 2015-10-12 clarified antiquotation;
2015-10-12 wenzelm 2015-10-12 spelling;
2015-10-12 wenzelm 2015-10-12 unused;
2015-10-12 wenzelm 2015-10-12 obsolete;
2015-10-12 wenzelm 2015-10-12 @{verbatim [display]} supersedes old alltt/ttbox;
2015-10-12 wenzelm 2015-10-12 @{verbatim [display]} supersedes old alltt/ttbox;
2015-10-12 wenzelm 2015-10-12 more symbols;
2015-10-12 wenzelm 2015-10-12 some control symbols for markup and formatting;
2015-10-12 wenzelm 2015-10-12 allow control symbols within markup body;
2015-10-12 wenzelm 2015-10-12 added glyphs 0x2501, 0x2508, 0x2509, 0x25aa, 0x25b8 from DejaVuSansMono;
2015-10-11 wenzelm 2015-10-11 proper document source;