etc/isar-keywords-ZF.el
2014-08-10 wenzelm 2014-08-10 support for named collections of theorems in canonical order;
2014-06-30 wenzelm 2014-06-30 removed obsolete Isar system commands -- raw ML console is normally used for system tinkering;
2014-06-27 wenzelm 2014-06-27 command 'print_term_bindings' supersedes 'print_binds';
2014-04-19 wenzelm 2014-04-19 added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
2014-03-25 wenzelm 2014-03-25 added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
2014-03-14 wenzelm 2014-03-14 discontinued somewhat pointless "thy_script" keyword kind;
2014-03-12 wenzelm 2014-03-12 simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser; added command 'print_ML_antiquotations';
2014-02-10 wenzelm 2014-02-10 discontinued axiomatic 'classes', 'classrel', 'arities';
2013-07-07 wenzelm 2013-07-07 discontinued command 'print_drafts';
2013-06-25 wenzelm 2013-06-25 misc tuning and clarification;
2013-06-24 wenzelm 2013-06-24 improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first; tuned signature;
2013-06-24 wenzelm 2013-06-24 back to keyword 'pr' :: diag as required for ProofGeneral command line -- reject this TTY command in Isabelle/jEdit by other means;
2013-06-24 wenzelm 2013-06-24 more formal ProofGeneral command setup within theory Pure; consider 'ProofGeneral.pr' as control command as well;
2013-06-23 wenzelm 2013-06-23 proper diagnostic command 'print_state';
2013-05-25 wenzelm 2013-05-25 syntax translations always depend on context;
2013-05-17 wenzelm 2013-05-17 renamed 'print_configs' to 'print_options';
2013-03-30 wenzelm 2013-03-30 added 'print_defn_rules' command; tuned;
2013-02-28 wenzelm 2013-02-28 discontinued obsolete 'axioms' command;
2013-02-27 wenzelm 2013-02-27 discontinued redundant 'use' command;
2013-02-27 wenzelm 2013-02-27 discontinued obsolete 'uses' within theory header;
2013-02-25 wenzelm 2013-02-25 reconsider 'pretty_setmargin' as "control" command (instead of "diag") -- it is stateful and Proof General legacy;
2012-09-26 wenzelm 2012-09-26 updated keywords;
2012-08-20 wenzelm 2012-08-20 some support for inlining file content into outer syntax token language;
2012-08-07 wenzelm 2012-08-07 prefer static Build.outer_syntax in Isabelle/Scala session -- discontinued incremental protocol; just one cumulative Keyword.status at end of batch session;
2012-03-21 wenzelm 2012-03-21 more explicit Toplevel.open_target/close_target; replaced 'context_includes' by 'context' 'includes'; tuned command descriptions;
2012-03-21 wenzelm 2012-03-21 basic support for nested contexts including bundles; include multiple bundles; renamed "affirm" back to "assert" (cf. c4492c6bf450 which was motivated by obsolete Alice/ML); tuned signatures;
2012-03-20 wenzelm 2012-03-20 basic support for bundled declarations;
2012-03-16 wenzelm 2012-03-16 eliminated odd 'finalconsts' / Theory.add_finals;
2012-03-15 wenzelm 2012-03-15 some support for outer syntax keyword declarations within theory header; more uniform Thy_Header.header as argument for begin_theory etc.;
2011-10-13 wenzelm 2011-10-13 discontinued obsolete 'types' command;
2011-08-16 wenzelm 2011-08-16 updated keywords -- old codegen is no longer in Pure;
2011-01-06 ballarin 2011-01-06 Diagnostic command to show locale dependencies.
2010-12-17 wenzelm 2010-12-17 Command 'type_synonym' (with single argument) supersedes 'types' (legacy feature);
2010-12-17 wenzelm 2010-12-17 replaced command 'nonterminals' by slightly modernized version 'nonterminal';
2010-12-05 wenzelm 2010-12-05 command 'notepad' replaces former 'example_proof';
2010-12-04 wenzelm 2010-12-04 formal notepad without any result;
2010-11-28 wenzelm 2010-11-28 added 'syntax_declaration' command;
2010-11-06 wenzelm 2010-11-06 updated keywords;
2010-09-10 wenzelm 2010-09-10 updated keywords;
2010-08-27 wenzelm 2010-08-27 discontinued separate Pure-ProofGeneral keywords session -- protocol commands are already defined in Pure;
2010-08-25 wenzelm 2010-08-25 discontinued obsolete 'global' and 'local' commands;
2010-08-17 wenzelm 2010-08-17 updated keywords;
2010-08-06 wenzelm 2010-08-06 updated keywords;
2010-07-28 wenzelm 2010-07-28 explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents;
2010-07-27 wenzelm 2010-07-27 updated keywords;
2010-04-29 wenzelm 2010-04-29 ProofContext.read_const: allow for type constraint (for fixed variable); added proof command 'write' to introduce concrete syntax within a proof body;
2010-04-28 wenzelm 2010-04-28 updated keywords;
2010-04-26 wenzelm 2010-04-26 command 'example_proof' opens an empty proof body;
2010-04-23 wenzelm 2010-04-23 updated generated files;
2010-04-16 wenzelm 2010-04-16 updated keywords;
2010-04-11 haftmann 2010-04-11 updated keywords
2010-03-01 wenzelm 2010-03-01 updated generated files;
2010-02-22 Cezary Kaliszyk 2010-02-22 update the keywords files
2009-11-23 wenzelm 2009-11-23 updated keywords;
2009-11-14 wenzelm 2009-11-14 updated keywords;
2009-10-23 blanchet 2009-10-23 updated keyword files to include "nitpick" and "nitpick_params"
2009-09-29 ballarin 2009-09-29 Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
2009-05-12 haftmann 2009-05-12 updated keywords
2009-05-11 bulwahn 2009-05-11 fixed code_pred command
2009-05-11 bulwahn 2009-05-11 Added pred_code command