2015-11-14 haftmann 2015-11-14 separate ML module for interpretation
2015-11-13 wenzelm 2015-11-13 support for structure statements in 'assume', 'presume';
2015-11-09 wenzelm 2015-11-09 uniform mandatory qualifier for all locale expressions, including 'statespace' parent; removed obsolete '!' syntax;
2015-11-04 ballarin 2015-11-04 Keyword 'rewrites' identifies rewrite morphisms.
2015-11-04 ballarin 2015-11-04 Qualifiers in locale expressions default to mandatory regardless of the command.
2015-10-17 wenzelm 2015-10-17 tuned signature;
2015-10-06 wenzelm 2015-10-06 added 'proposition' command;
2015-10-06 wenzelm 2015-10-06 fewer aliases for toplevel theorem statements;
2015-10-06 wenzelm 2015-10-06 just one theorem kind, which is legacy anyway;
2015-09-25 wenzelm 2015-09-25 proper context;
2015-09-23 wenzelm 2015-09-23 tuned signature;
2015-09-22 wenzelm 2015-09-22 separate command 'print_definitions';
2015-09-22 wenzelm 2015-09-22 HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015; defs.ML: track dependencies also for type constructors; typedef.ML: add type defined by typedef to dependencies, Abs and Rep now depend on the type; Pure types and typedecls are final -- no dependencies;
2015-09-21 wenzelm 2015-09-21 separate panel for proof state output;
2015-08-17 wenzelm 2015-08-17 support for ML files with/without debugger information;
2015-08-17 wenzelm 2015-08-17 explicit debug flag for ML compiler;
2015-08-06 wenzelm 2015-08-06 evaluate ML expressions within debugger context; redirected writeln/warning for ML compiler;
2015-07-08 wenzelm 2015-07-08 more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
2015-07-02 wenzelm 2015-07-02 allow to specify suffix of goal parameters;
2015-07-02 wenzelm 2015-07-02 subgoal parameters are internal by default and named by user;
2015-07-01 wenzelm 2015-07-01 support for subgoal focus command;
2015-06-24 wenzelm 2015-06-24 clarified 'case' command;
2015-06-22 wenzelm 2015-06-22 support 'when' statement, which corresponds to 'presume';
2015-06-13 wenzelm 2015-06-13 tuned signature;
2015-06-13 wenzelm 2015-06-13 clarified 'obtain', using structured 'have' statement;
2015-06-13 wenzelm 2015-06-13 renamed "prems" to "that";
2015-06-11 wenzelm 2015-06-11 support for 'consider' command; allow full "fixes" for 'obtain' command; tuned signature;
2015-06-10 wenzelm 2015-06-10 support for "if prems" in local goal statements;
2015-06-09 wenzelm 2015-06-09 allow for_fixes for 'have', 'show' etc.; tuned signature;
2015-06-07 wenzelm 2015-06-07 tuned signature;
2015-06-05 wenzelm 2015-06-05 added Isar command 'supply';
2015-05-07 wenzelm 2015-05-07 use display_graph_old for locale_deps, to show a bit more than nothing for cyclic graphs;
2015-04-22 wenzelm 2015-04-22 tuned signature;
2015-04-16 wenzelm 2015-04-16 tuned;
2015-04-16 wenzelm 2015-04-16 discontinued pointless warnings: commands are only defined inside a theory context;
2015-04-16 wenzelm 2015-04-16 clarified thy_deps;
2015-04-06 wenzelm 2015-04-06 @{command_spec} is superseded by @{command_keyword};
2015-04-06 wenzelm 2015-04-06 clarified command keyword markup;
2015-04-06 wenzelm 2015-04-06 tuned signature;
2015-04-04 wenzelm 2015-04-04 support private scope for individual local theory commands; tuned signature;
2015-04-03 wenzelm 2015-04-03 more uniform "verbose" option to print name space;
2015-04-01 wenzelm 2015-04-01 added command 'experiment';
2015-04-01 wenzelm 2015-04-01 tuned signature;
2014-11-30 wenzelm 2014-11-30 more abstract type Input.source;
2014-11-22 wenzelm 2014-11-22 more careful ML source positions, for improved PIDE markup;
2014-11-13 wenzelm 2014-11-13 uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style; discontinued obsolete 'txt_raw' (superseded by 'text_raw'); eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds); 'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind; changed tagging of diagnostic commands within proof;
2014-11-11 wenzelm 2014-11-11 more position information, e.g. relevant for errors in generated ML source;
2014-11-07 wenzelm 2014-11-07 tuned signature;
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-11-03 wenzelm 2014-11-03 eliminated unused int_only flag (see also c12484a27367); just proper commands;
2014-11-02 wenzelm 2014-11-02 clarified legacy command;
2014-11-02 wenzelm 2014-11-02 uniform heading commands work in any context, even in theory header; discontinued obsolete 'sect', 'subsect', 'subsubsect'; marked obsolete 'header' as legacy;
2014-11-01 wenzelm 2014-11-01 tuned signature, in accordance to Scala version;
2014-10-31 wenzelm 2014-10-31 discontinued Isar TTY loop;
2014-10-31 wenzelm 2014-10-31 removed obsolete Proof General commands;
2014-10-28 wenzelm 2014-10-28 'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;
2014-09-07 haftmann 2014-09-07 separated class_deps command into separate file
2014-08-21 wenzelm 2014-08-21 tuned signature -- define some elementary operations earlier;
2014-08-14 wenzelm 2014-08-14 localized command 'method_setup' and 'attribute_setup'; clarified (non)application of morphism: argument src is already transformed, semantic body remains untransformed;
2014-08-14 wenzelm 2014-08-14 tuned signature -- prefer self-contained user-space tool;