2014-03-10 wenzelm 2014-03-10 include long identifiers in the reckoning of words (e.g. "integer.lifting" vs. 'lifting_update');
2014-03-10 wenzelm 2014-03-10 tuned messages -- in accordance to Isabelle/Scala;
2014-03-10 wenzelm 2014-03-10 tuned;
2014-03-10 wenzelm 2014-03-10 enabled test in PIDE interaction;
2014-03-10 wenzelm 2014-03-10 proper Args.syntax for slightly odd bundle trickery; do not handle arbitrary exceptions; more abstract type Args.src;
2014-03-10 wenzelm 2014-03-10 some Markup.language_path to prevent completion of symbols (notably "~") -- always "delimited" for simplicity in contrast to 42ac3cfb89f6;
2014-03-10 wenzelm 2014-03-10 more markup;
2014-03-10 wenzelm 2014-03-10 clarified Args.check_src: retain name space information for error output; tuned signature;
2014-03-10 wenzelm 2014-03-10 tuned;
2014-03-10 wenzelm 2014-03-10 modernized data managed via Name_Space.table;
2014-03-10 wenzelm 2014-03-10 clarified Args.src: more abstract type, position refers to name only; prefer self-contained Args.check_src;
2014-03-10 wenzelm 2014-03-10 tuned signature;
2014-03-10 wenzelm 2014-03-10 prefer Name_Space.pretty with its builtin markup;
2014-03-10 wenzelm 2014-03-10 tuned signature -- prefer Name_Space.get with its builtin error;
2014-03-10 wenzelm 2014-03-10 abstract type Name_Space.table; clarified pretty_locale_deps: sort strings; clarified Proof_Context.update_cases: Name_Space.del_table hides name space entry as well;
2014-03-10 wenzelm 2014-03-10 more structured order;
2014-03-10 wenzelm 2014-03-10 more direct Long_Name.qualification;
2014-03-10 wenzelm 2014-03-10 more restrictive completion: intern/extern stability;
2014-03-10 hoelzl 2014-03-10 add measurability rule for (co)inductive predicates
2014-03-10 hoelzl 2014-03-10 introduced antimono; incseq, decseq are now abbreviations for mono and antimono; renamed Library/Continuity to Library/Order_Continuity; removed up_cont; renamed down_cont to down_continuity and generalized to complete_lattices
2014-03-10 kuncar 2014-03-10 hide implementation details
2014-03-10 traytel 2014-03-10 copy-paste typo
2014-03-10 traytel 2014-03-10 tuned tactic
2014-03-10 traytel 2014-03-10 unfold intermediate definitions after sealing the bnf
2014-03-09 haftmann 2014-03-09 bootstrap fundamental Fun theory immediately after Set theory, without dependency on complete lattices * * * tuned
2014-03-09 haftmann 2014-03-09 tuned; elimination rule subset_imageE; typical composition collapsing rewrite order in lemma image_image_eq_image_comp; destruction rules ball_imageD, bex_imageD
2014-03-09 traytel 2014-03-09 more careful unfolding of internal constants
2014-03-09 traytel 2014-03-09 made typedef for the type of the bound optional (size-based)
2014-03-07 traytel 2014-03-07 made natLe{q,ss} constants (yields smaller terms in composition)
2014-03-07 traytel 2014-03-07 removed junk
2014-03-09 wenzelm 2014-03-09 tuned proofs;
2014-03-09 wenzelm 2014-03-09 unused;
2014-03-09 wenzelm 2014-03-09 tuned;
2014-03-09 wenzelm 2014-03-09 more formal read_root;
2014-03-09 wenzelm 2014-03-09 simplified / modernized hide commands: proper outer parsers and PIDE markup via check;
2014-03-09 wenzelm 2014-03-09 removed dead code;
2014-03-09 wenzelm 2014-03-09 check fact names with PIDE markup;
2014-03-09 wenzelm 2014-03-09 tuned signature;
2014-03-09 wenzelm 2014-03-09 do allow replacement of words where this is appropriate, notably symbol abbrevs and keyword templates (see also 1c42ebdb3a58);
2014-03-08 wenzelm 2014-03-08 tuned proofs;
2014-03-08 wenzelm 2014-03-08 tuned proofs;
2014-03-08 wenzelm 2014-03-08 keep current context visibility for PIDE markup and completion (in contrast to 8e3e004f1c31): Attrib.check_src of 9dc5ce83202c should intern/report attributes once, which happens for local_theory in the (visible) auxiliary context;
2014-03-08 wenzelm 2014-03-08 modernized Attrib.check_name/check_src similar to methods (see also a989bdaf8121); proper context for global data; tuned signature;
2014-03-08 wenzelm 2014-03-08 allow suffix of underscores for words (notably keywords), similar to semantic completion;
2014-03-08 wenzelm 2014-03-08 back to polyml-svn, with more threads to avoid problems with HOL-Proofs (see f376f18fd0b7);
2014-03-08 wenzelm 2014-03-08 no completion for complete keywords, to avoid confusion of 'assume' ~> 'assumes' etc.;
2014-03-08 wenzelm 2014-03-08 clarified description; tuned;
2014-03-08 wenzelm 2014-03-08 tuned;
2014-03-07 wenzelm 2014-03-07 tuned proofs;
2014-03-07 wenzelm 2014-03-07 more antiquotations;
2014-03-07 wenzelm 2014-03-07 ignore special names that are treated differently for various sub-languages (main wild-card is identifier "__");
2014-03-07 wenzelm 2014-03-07 merged
2014-03-07 wenzelm 2014-03-07 misc tuning;
2014-03-07 wenzelm 2014-03-07 more strict discrimination: symbols vs. keywords could overlap;
2014-03-07 wenzelm 2014-03-07 tuned;
2014-03-07 wenzelm 2014-03-07 more accurate description;
2014-03-07 wenzelm 2014-03-07 misc tuning and clarification;
2014-03-07 wenzelm 2014-03-07 more accurate description;
2014-03-07 wenzelm 2014-03-07 tuned proofs;
2014-03-07 wenzelm 2014-03-07 tuned;