tuned

more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;

updated to jedit-5.3.0 and SideKick 1.8;

updated to jdk-8u66;

print thm wrt. local shyps (from full proof context); tuned;

clarified modules; tuned signature;

proper transfer of stored facts;

tuned;

more robust ASCII output: avoid ligatures of quotes;

tuned;

more control symbols; tuned;

clarified scan_cartouche_depth (amending 8284c0d5bf52): finish after outermost cartouche;

rendering for \<^verbatim>;

Isabelle fonts via external component;

tuned document;

tuned document;

added glyphs 0x25a9 from DejaVuSansMono;

removed generated files from repository;

tuned;

proper spaces around @{text};

isabelle update_cartouches -t;

added isabelle update_cartouches option -t;

another antiquotation short form: undecorated cartouche as alias for @{text}; document antiquotation @{text} ignores option "source";

repaired document;

more symbols; tunes whitespace;

tuned English;

more symbols, with swapped defaults: old-style ASCII syntax uses "ASCII" print mode;

tuned document;

merged

avoid odd permissions of fresh tmp_file;

added action "isabelle-emph"; changed shortcut of action "isabelle-reset";

tuned;

tuned;

tuned text

tuned;

merged

more control symbols;

tuned signature;

tuned signature;

clarified;

clarified control antiquotations: decode control symbol to get name; document antiquotations @{emph}, @{bold}; symbol interpretation for \<^emph>; tuned;

more documentation;

support control symbol antiquotations;

clarified Symbol.is_control;

added 2-3 trees (simpler and more complete than the version in ex/Tree23)

code abbreviation for mapping over a fixed range

back to lxbroy3, which appears to be free at the moment;

tuned signature;

merged

more uniform command setup;

added 'paragraph', 'subparagraph';

clarified Latex.environment;

more explicit output of list items;

tuned;

clarified nesting of paragraphs: indentation is taken into account more uniformly; tuned;

Markdown support in document text;

clarified Antiquote.antiq_reports; Thy_Output.output_text: support for markdown (inactive); eliminared Thy_Output.check_text -- uniform use of Thy_Output.output_text;

trim_blanks after read, before eval; clarified Raw_Token: uniform output_text; tuned signature;

clarified modules;

load markdown.ML into Pure;

proper recursive nesting of adjacent lists;

tuned;

clarified line content: source without marker prefix;

more markup;

report Markdown document structure;

more comments;

unused -- avoid confusion in Symbols dockable;

proper nesting of adjacent lists;

more document structure; tuned signature;

more document structure;

more document structure;

clarified;

minimal support for Markdown documents;

clarified;

more symbols;

more symbols;

clarified control symbols;

added glyphs 0x21e4, 0x21e5, 0x27a7 from DejaVuSansMono;

tuned signature (cf. XML.trim_blanks);

added split_lines; tuned signature;

qualify some names stemming from internal bootstrap constructions

removed too aggressive underscorization

typo

prefer undecorated typedef

even -> evn to avoid clash with global even

added invar empty

Fixed nonterminating "blast" proof

new material on path_component_sets, inside, outside, etc. And more default simprules

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

prod_case as canonical name for product type eliminator

emphasized general nature of parameter

moved lemmas

more symbols;

redundant due to \parindent 0pt;

isabelle update_cartouches;

scalable fonts for T1 encoding;

proper imports; more symbols; avoid special latex tricks;

more symbols;

more symbols;

more antiquotations;

proper message;

clarified antiquotation;

spelling;

unused;

obsolete;

@{verbatim [display]} supersedes old alltt/ttbox;

@{verbatim [display]} supersedes old alltt/ttbox;

more symbols;

some control symbols for markup and formatting;

allow control symbols within markup body;

added glyphs 0x2501, 0x2508, 0x2509, 0x25aa, 0x25b8 from DejaVuSansMono;

proper document source;