src/Pure/Pure.thy
2016-04-26 ago 'obtain' supports structured statements (similar to 'define');
2016-04-25 ago old 'def' is legacy;
2016-04-24 ago added Isar command 'define';
2016-04-13 ago eliminated "xname" and variants;
2016-04-10 ago more standard session build process, including browser_info;
2016-04-08 ago eliminated unused simproc identifier;
2016-04-07 ago more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
2016-04-07 ago Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
2016-04-05 ago support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
2016-04-05 ago tuned;
2016-04-04 ago more uniform ML file commands;
2016-04-04 ago tuned whitespace;
2016-04-04 ago tuned -- more explicit sections;
2016-04-04 ago clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
2016-04-04 ago clarified bootstrap -- more uniform use of ML files;
2016-03-01 ago ML debugger support in Pure (again, see 3565c9f407ec);
2016-02-14 ago command '\<proof>' is an alias for 'sorry', with different typesetting;
2016-01-13 ago removed old 'defs' command;
2015-12-19 ago abandoned attempt to unify sublocale and interpretation into global theories
2015-12-16 ago rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
2015-11-14 ago prefer "rewrites" and "defines" to note rewrite morphisms
2015-11-14 ago coalesce permanent_interpretation.ML with interpretation.ML
2015-11-10 ago clarified modules;
2015-11-05 ago symbolic syntax "\<comment> text";
2015-11-04 ago Keyword 'rewrites' identifies rewrite morphisms.
2015-10-06 ago added 'proposition' command;
2015-10-06 ago fewer aliases for toplevel theorem statements;
2015-09-22 ago separate command 'print_definitions';
2015-08-17 ago support for ML files with/without debugger information;
2015-07-17 ago skeleton for interactive debugger;
2015-07-08 ago clarified text folds: proof ... qed counts as extra block;
2015-07-01 ago clarified keyword categories;
2015-07-01 ago support for subgoal focus command;
2015-06-22 ago support 'when' statement, which corresponds to 'presume';
2015-06-11 ago support for 'consider' command;
2015-06-05 ago added Isar command 'supply';
2015-05-30 ago unused;
2015-04-16 ago clarified thy_deps;
2015-04-09 ago clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
2015-04-06 ago support for 'restricted' modifier: only qualified accesses outside the local scope;
2015-04-04 ago support private scope for individual local theory commands;
2015-04-01 ago added command 'experiment';
2014-11-13 ago uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
2014-11-07 ago plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
2014-11-06 ago simplified keyword kinds;
2014-11-02 ago uniform heading commands work in any context, even in theory header;
2014-11-01 ago eliminated spurious semicolons;
2014-10-31 ago discontinued Isar TTY loop;
2014-10-31 ago removed obsolete Proof General commands;
2014-10-31 ago discontinued Proof General;
2014-10-28 ago explicit keyword category for commands that may start a block;
2014-10-13 ago clarified load order;
2014-10-13 ago support for named plugins for definitional packages;
2014-10-07 ago more symbols;
2014-10-07 ago more cartouches;
2014-10-05 ago bibtex support in ML: document antiquotation @{cite} with markup;
2014-09-07 ago separated class_deps command into separate file
2014-08-14 ago tuned signature -- prefer self-contained user-space tool;
2014-08-10 ago support for named collections of theorems in canonical order;
2014-07-04 ago suppress completion of obscure keyword;