etc/isar-keywords.el
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-25 wenzelm 2013-05-25 updated keywords;
2013-05-17 wenzelm 2013-05-17 renamed 'print_configs' to 'print_options';
2013-04-30 blanchet 2013-04-30 renamed "bnf_def" keyword to "bnf" (since it's not a definition, but rather a registration)
2013-04-29 blanchet 2013-04-29 renamed BNF "(co)data" commands to names that are closer to their final names
2013-04-26 blanchet 2013-04-26 updated keywords
2013-04-10 wenzelm 2013-04-10 updated keywords;
2013-03-30 wenzelm 2013-03-30 added 'print_defn_rules' command; tuned;
2013-03-08 wenzelm 2013-03-08 updated keywords (cf. 84d01fd733cf);
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 'export_code' as "thy_decl" command due to its global side-effect on the file-system;
2013-02-25 wenzelm 2013-02-25 reconsider 'pretty_setmargin' as "control" command (instead of "diag") -- it is stateful and Proof General legacy;
2012-11-30 wenzelm 2012-11-30 added 'print_inductives' command;
2012-11-17 wenzelm 2012-11-17 updated keywords;
2012-09-28 wenzelm 2012-09-28 updated keywords using proper "isabelle update_keywords";
2012-09-28 blanchet 2012-09-28 killed temporary "data_raw" and "codata_raw" now that the examples have been ported to "data" and "codata"
2012-09-28 blanchet 2012-09-28 compatibility option to use "rep_datatype"
2012-09-26 wenzelm 2012-09-26 updated keywords;
2012-09-21 blanchet 2012-09-21 renamed "Codatatype" directory "BNF" (and corresponding session) -- this opens the door to no-nonsense session names like "HOL-BNF-LFP"
2012-09-11 wenzelm 2012-09-11 updated keywords;
2012-09-04 blanchet 2012-09-04 started work on sugared "(co)data" commands
2012-09-03 blanchet 2012-09-03 renamed three BNF/(co)datatype-related commands
2012-08-30 blanchet 2012-08-30 more work on BNF sugar -- up to derivation of nchotomy
2012-08-30 blanchet 2012-08-30 killed obsolete "bnf_of_typ" command
2012-08-28 wenzelm 2012-08-28 more permanent update of keywords (cf. 3517d6f50b12);
2012-08-28 blanchet 2012-08-28 updated keywords
2012-08-23 wenzelm 2012-08-23 added specific 'spark_open_vcg' and 'spark_open_siv' with formal management of corresponding source files;
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-04-04 huffman 2012-04-04 update keywords file
2012-04-03 kuncar 2012-04-03 new package Lifting - initial commit
2012-04-01 krauss 2012-04-01 merged, manually resolving conflicts due to session renaming (cf. 6488c5efec49)
2012-04-01 wenzelm 2012-04-01 more keywords;
2012-03-23 kuncar 2012-03-23 update etc/isar-keywords.el
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 more precise TPTP keywords and dependencies;
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.;
2012-02-24 blanchet 2012-02-24 renamed 'try_methods' to 'try0'
2012-02-22 bulwahn 2012-02-22 adding new command "find_unused_assms"
2011-12-20 bulwahn 2011-12-20 added keywords
2011-10-19 wenzelm 2011-10-19 updated keywords;
2011-10-13 wenzelm 2011-10-13 discontinued obsolete 'types' command;
2011-09-23 berghofe 2011-09-23 Include keywords print_coercions and print_coercion_maps
2011-08-16 wenzelm 2011-08-16 include HOL-Library keywords for the sake of recdef;
2011-05-27 blanchet 2011-05-27 added "try" command, to launch Solve Direct, Quickcheck, Nitpick, Sledgehammer, and Try Methods
2011-04-15 berghofe 2011-04-15 Added command for associating user-defined types with SPARK types.
2011-01-15 berghofe 2011-01-15 Include HOL-SPARK keywords
2011-01-12 wenzelm 2011-01-12 updated keywords;
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-06 haftmann 2010-12-06 replace `type_mapper` by the more adequate `type_lifting`
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;