2014-02-25 wenzelm 2014-02-25 more completion rendering: active, semantic, syntactic; tuned;
2014-02-25 wenzelm 2014-02-25 tuned;
2014-02-25 wenzelm 2014-02-25 tuned message -- more markup;
2014-02-25 wenzelm 2014-02-25 clarified token markup: keyword1/keyword2 is for syntax, and "command" the entity kind; tuned message;
2014-02-25 wenzelm 2014-02-25 proper context for global data;
2014-02-25 wenzelm 2014-02-25 modernized Method.check_name/check_source (with reports) vs. strict Method.the_method (without interning nor reports), e.g. relevant for semantic completion; removed obsolete Method.Source_i; proper context for global data; tuned messages;
2014-02-25 wenzelm 2014-02-25 optimize special case according to Library.merge (see also 8fbc355100f2); no treatment for Net.merge, due to non-standard merge order;
2014-02-25 wenzelm 2014-02-25 more positions; tuned messages;
2014-02-25 wenzelm 2014-02-25 more markup;
2014-02-25 kuncar 2014-02-25 simplify a proof due to 6c95a39348bd
2014-02-25 kuncar 2014-02-25 new rule for making rsp theorem more readable
2014-02-25 kuncar 2014-02-25 unregister lifting setup following the best practice of Lifting
2014-02-25 paulson 2014-02-25 generalised some results using type classes
2014-02-25 paulson 2014-02-25 More complex-related lemmas
2014-02-25 kuncar 2014-02-25 the rules are not needed due to 1726f46d2aa8
2014-02-25 kuncar 2014-02-25 simplify and repair proofs due to df0fda378813
2014-02-25 kuncar 2014-02-25 rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
2014-02-24 paulson 2014-02-24 Gauss.thy ported from Old_Number_Theory (unfinished)
2014-02-24 wenzelm 2014-02-24 merged
2014-02-24 wenzelm 2014-02-24 reverted c05d3e22adaf: Locale.intern is still required by AFP/Simpl;
2014-02-24 wenzelm 2014-02-24 optimize special case according to Library.merge (see also 8fbc355100f2, 520872460b7b);
2014-02-24 wenzelm 2014-02-24 tuned colors;
2014-02-24 wenzelm 2014-02-24 prefer standard Proof_Context.transfer, with theory stamp transfer (should now work thanks to purely functional theory, without Theory.copy etc.);
2014-02-24 kuncar 2014-02-24 more robust registration of code equations
2014-02-24 kuncar 2014-02-24 be consistent and produce always rep_eq with =
2014-02-24 kuncar 2014-02-24 publish a useful function
2014-02-24 kuncar 2014-02-24 don't be so aggresive for a public test function and raise only BAD_THM instead of ERROR
2014-02-24 kuncar 2014-02-24 add missing attributes
2014-02-24 paulson 2014-02-24 Lemmas about Reals, norm, etc., and cleaner variants of existing ones
2014-02-24 paulson 2014-02-24 A few lemmas about summations, etc.
2014-02-24 wenzelm 2014-02-24 merged
2014-02-24 wenzelm 2014-02-24 tuned;
2014-02-24 wenzelm 2014-02-24 tuned messages -- prefer quote before Position.here, which might be just \<here>;
2014-02-24 wenzelm 2014-02-24 clarified ML language flags;
2014-02-24 wenzelm 2014-02-24 clarified painting of invisible caret, e.g. focus change due to popup;
2014-02-24 wenzelm 2014-02-24 tuned signature -- weaker type requirement;
2014-02-24 wenzelm 2014-02-24 paint completion range of active popup;
2014-02-24 wenzelm 2014-02-24 tuned messages;
2014-02-24 wenzelm 2014-02-24 clarified Token.range_of in accordance to Symbol_Pos.range; eliminated redundant Position.set_range, which is already included in Position.range;
2014-02-24 wenzelm 2014-02-24 tuned signature;
2014-02-24 traytel 2014-02-24 clarified interaction with dead variables in the composition of BNFs
2014-02-24 blanchet 2014-02-24 added BNF cache (within one definition)
2014-02-23 blanchet 2014-02-23 updated docs
2014-02-23 blanchet 2014-02-23 optimized 'bnf_of_typ' further w.r.t. dead variables
2014-02-23 blanchet 2014-02-23 optimization of 'bnf_of_typ' if all variables are dead
2014-02-23 blanchet 2014-02-23 improved accounting for dead variables when naming set functions (refines d71c2737ee21)
2014-02-23 blanchet 2014-02-23 added explicit killing
2014-02-23 blanchet 2014-02-23 more precise error message
2014-02-23 blanchet 2014-02-23 reuse same parser for '(co)datatype(_new)' as for 'bnf_decl'
2014-02-23 wenzelm 2014-02-23 tuned message;
2014-02-23 wenzelm 2014-02-23 tuned proofs;
2014-02-23 wenzelm 2014-02-23 tuned whitespace;
2014-02-23 wenzelm 2014-02-23 unused;
2014-02-23 wenzelm 2014-02-23 clarified semantic completion: retain kind.full_name as official item name for history; misc tuning;
2014-02-23 wenzelm 2014-02-23 try explicit semantic completion before syntax completion;
2014-02-23 wenzelm 2014-02-23 more explicit Completion.Item.range, independently of caret;
2014-02-23 wenzelm 2014-02-23 tuned whitespace;
2014-02-23 wenzelm 2014-02-23 clarified stretch_point_range wrt. UTF-16 surrogates; tuned;
2014-02-23 wenzelm 2014-02-23 tuned;
2014-02-23 wenzelm 2014-02-23 some rendering of completion range; tuned;