2012-10-17 wenzelm 2012-10-17 more formal markup;
2012-08-02 wenzelm 2012-08-02 more official command specifications, including source position;
2012-03-17 wenzelm 2012-03-17 sort via string_ord (as secondary key), not fast_string_ord via Symtab.fold; tuned;
2012-03-16 wenzelm 2012-03-16 outer syntax command definitions based on formal command_spec derived from theory header declarations;
2012-02-27 wenzelm 2012-02-27 discontinued slightly odd built-in timing (cf. 53fd5cc685b4) -- the Isar toplevel does that already (e.g. via Toplevel.timing or Toplevel.profiling);
2012-02-27 wenzelm 2012-02-27 prefer uniform Timing.message -- avoid assumption about sequential execution;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-20 wenzelm 2011-03-20 structure Timing: covers former start_timing/end_timing and Output.timeit etc; explicit Timing.message function; eliminated Output.timing flag, cf. Toplevel.timing; tuned;
2010-08-11 wenzelm 2010-08-11 standardized pretty printing of consts (e.g. see find_theorems, print_theory);
2010-08-11 wenzelm 2010-08-11 misc tuning and simplification;
2010-08-11 wenzelm 2010-08-11 simplified/unified command setup;
2010-05-15 wenzelm 2010-05-15 renamed structure OuterSyntax to Outer_Syntax, keeping the old name as alias for some time;
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2009-10-29 wenzelm 2009-10-29 less hermetic ML; parse_pattern: apply Consts.intern only once (Why is this done anyway?); modernized structure names;
2009-10-25 wenzelm 2009-10-25 conceal consts via name space, not tags;
2009-09-30 wenzelm 2009-09-30 handle Type.TYPE_MATCH, not arbitrary exceptions;
2009-06-17 wenzelm 2009-06-17 more detailed start_timing/end_timing;
2009-06-17 wenzelm 2009-06-17 minor tuning according to Isabelle/ML conventions; slightly less combinators;
2009-03-03 Timothy Bourke 2009-03-03 Implement Makarius's suggestion for improved type pattern parsing.
2009-03-02 Timothy Bourke 2009-03-02 find_consts: fold in preference to foldl; hide internal constants; remove redundant exception catch
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-03-01 wenzelm 2009-03-01 avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;
2009-02-27 wenzelm 2009-02-27 observe basic Isabelle/ML coding conventions;
2009-02-27 wenzelm 2009-02-27 moved find_theorems.ML and find_consts.ML to Pure/Tools, collecting main implementation in one place each;