2008-08-15 wenzelm 2008-08-15 removed redundant "symbol" property; added "font" propery; disabled alternative letters (\<A> etc.) for now;
2008-08-15 wenzelm 2008-08-15 Default interpretation of some Isabelle symbols.
2008-08-15 wenzelm 2008-08-15 report antiquotation names; tuned messages;
2008-08-15 wenzelm 2008-08-15 fixed DOCTYPE -- XHTML is case-sensitive!
2008-08-15 wenzelm 2008-08-15 report antiquotation names;
2008-08-15 wenzelm 2008-08-15 added ML_antiq, doc_antiq;
2008-08-15 wenzelm 2008-08-15 added README;
2008-08-15 wenzelm 2008-08-15 generated truetype font;
2008-08-15 wenzelm 2008-08-15 The Jerusalem font from 2004 -- unicode version.
2008-08-15 wenzelm 2008-08-15 args: explicit groups for file_name, theory_name;
2008-08-15 wenzelm 2008-08-15 read_asts: Lexicon.report_token, filter Lexicon.is_proper; report tokens;
2008-08-15 wenzelm 2008-08-15 filter Lexicon.is_proper -- Lexicon.tokenize now includes improper tokens;
2008-08-15 wenzelm 2008-08-15 token_kind: add Space, Comment; tokenize: now includes improper tokens, cf. is_proper; added report_token;
2008-08-15 wenzelm 2008-08-15 renamed T.source_of' to T.source_position_of; tuned signature;
2008-08-15 wenzelm 2008-08-15 renamed T.source_of' to T.source_position_of;
2008-08-15 wenzelm 2008-08-15 output_markup: check Markup.is_none;
2008-08-15 wenzelm 2008-08-15 added is_none; added inner_comment;
2008-08-15 wenzelm 2008-08-15 Args.name_source(_position) for proper position information;
2008-08-14 wenzelm 2008-08-14 [source=false] for quoted antiquotation avoids quote-escapes in output;
2008-08-14 wenzelm 2008-08-14 report antiquotations;
2008-08-14 wenzelm 2008-08-14 tuned;
2008-08-14 wenzelm 2008-08-14 report ML_source;
2008-08-14 wenzelm 2008-08-14 renamed P.ml_source to P.ML_source;
2008-08-14 wenzelm 2008-08-14 report doc_source;
2008-08-14 wenzelm 2008-08-14 added ML_source, doc_source;
2008-08-14 wenzelm 2008-08-14 antiquotes: proper SymbolPos decoding, adapted Antiquote.read/Antiq;
2008-08-14 wenzelm 2008-08-14 added source_of';
2008-08-14 wenzelm 2008-08-14 P.doc_source and P.ml_sorce for proper SymbolPos.text;
2008-08-14 wenzelm 2008-08-14 oracle, header/local_theory/proof_markup: pass SymbolPos.text;
2008-08-14 wenzelm 2008-08-14 use SymbolPos.T list directly, instead of encoded SymbolPos.text;
2008-08-14 wenzelm 2008-08-14 ML_Context.add_antiq: pass position; @{lemma}: set source position;
2008-08-14 wenzelm 2008-08-14 ML_Context.add_antiq: pass position;
2008-08-14 wenzelm 2008-08-14 retrieve_thms: transfer fact position to result; tuned;
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm; added position operations; tuned;
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-08-14 wenzelm 2008-08-14 made SML/NJ happy;
2008-08-13 wenzelm 2008-08-13 removed obsolete present_html -- now part of regular theory presentation;
2008-08-13 wenzelm 2008-08-13 removed obsolete verbatim_source, results, chapter, section etc.; removed obsolete results, theorems(s); moved theorem result hook to proof_display.ML;
2008-08-13 wenzelm 2008-08-13 removed obsolete verbatim_source, results, chapter, section etc.; removed redundant end_index, end_theory;
2008-08-13 wenzelm 2008-08-13 ProofDisplay.add_hook;
2008-08-13 wenzelm 2008-08-13 simplified present_local_theory/proof;
2008-08-13 wenzelm 2008-08-13 ProofDisplay.theory_results;
2008-08-13 wenzelm 2008-08-13 removed obsolete present_results; added theory_results, which is subject to hooks (formerly in present.ML);
2008-08-13 wenzelm 2008-08-13 scan: SymbolPos.tabify_content when creating tokens (for proper presentation output);
2008-08-13 wenzelm 2008-08-13 load_thy: no untabify (preserve position information!), present spans instead of verbatim source;
2008-08-13 wenzelm 2008-08-13 simplified markup commands;
2008-08-13 wenzelm 2008-08-13 simplified markup commands -- removed obsolete Present.results, always check text;
2008-08-13 wenzelm 2008-08-13 added untabify_content;
2008-08-13 wenzelm 2008-08-13 tuned;
2008-08-13 wenzelm 2008-08-13 removed obsolete untabify (superceded by SymbolPos.tabify_content);
2008-08-13 wenzelm 2008-08-13 tuned document;
2008-08-13 wenzelm 2008-08-13 removed obsolete theorems; handle generic XML markup as well (plain <markup> instead of <... class=markup>); misc tuning/update according to Pure/Generic/markup.ML;
2008-08-13 berghofe 2008-08-13 Changed proof of strong induction rule to avoid infinite loop when premises of introduction rules contain equations.
2008-08-12 wenzelm 2008-08-12 token_kind_markup: complete coverage;
2008-08-12 wenzelm 2008-08-12 OuterSyntax.scan: pass position;
2008-08-12 wenzelm 2008-08-12 message: ignored if body empty;
2008-08-12 wenzelm 2008-08-12 load_thy: removed obsolete dir argument;
2008-08-12 wenzelm 2008-08-12 abstract type span, tuned interfaces; added report_token, report_span; markup ident tokens;
2008-08-12 wenzelm 2008-08-12 adapted ThyEdit operations;
2008-08-12 wenzelm 2008-08-12 added ignored, malformed transitions;