src/Pure/Pure.thy
2016-04-10 wenzelm 2016-04-10 more standard session build process, including browser_info; clarified final setup of global ML environment;
2016-04-08 wenzelm 2016-04-08 eliminated unused simproc identifier;
2016-04-07 wenzelm 2016-04-07 more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use'; avoid slowdown of Resources.loaded_files due to command name 'use' in Pure base syntax;
2016-04-07 wenzelm 2016-04-07 Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
2016-04-05 wenzelm 2016-04-05 support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
2016-04-05 wenzelm 2016-04-05 tuned;
2016-04-04 wenzelm 2016-04-04 more uniform ML file commands;
2016-04-04 wenzelm 2016-04-04 tuned whitespace;
2016-04-04 wenzelm 2016-04-04 tuned -- more explicit sections;
2016-04-04 wenzelm 2016-04-04 clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
2016-04-04 wenzelm 2016-04-04 clarified bootstrap -- more uniform use of ML files;
2016-03-01 wenzelm 2016-03-01 ML debugger support in Pure (again, see 3565c9f407ec);
2016-02-14 wenzelm 2016-02-14 command '\<proof>' is an alias for 'sorry', with different typesetting;
2016-01-13 wenzelm 2016-01-13 removed old 'defs' command;
2015-12-19 haftmann 2015-12-19 abandoned attempt to unify sublocale and interpretation into global theories
2015-12-16 wenzelm 2015-12-16 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 haftmann 2015-11-14 prefer "rewrites" and "defines" to note rewrite morphisms
2015-11-14 haftmann 2015-11-14 coalesce permanent_interpretation.ML with interpretation.ML
2015-11-10 wenzelm 2015-11-10 clarified modules;
2015-11-05 wenzelm 2015-11-05 symbolic syntax "\<comment> text";
2015-11-04 ballarin 2015-11-04 Keyword 'rewrites' identifies rewrite morphisms.
2015-10-06 wenzelm 2015-10-06 added 'proposition' command;
2015-10-06 wenzelm 2015-10-06 fewer aliases for toplevel theorem statements;
2015-09-22 wenzelm 2015-09-22 separate command 'print_definitions';
2015-08-17 wenzelm 2015-08-17 support for ML files with/without debugger information;
2015-07-17 wenzelm 2015-07-17 skeleton for interactive debugger;
2015-07-08 wenzelm 2015-07-08 clarified text folds: proof ... qed counts as extra block;
2015-07-01 wenzelm 2015-07-01 clarified keyword categories;
2015-07-01 wenzelm 2015-07-01 support for subgoal focus command;
2015-06-22 wenzelm 2015-06-22 support 'when' statement, which corresponds to 'presume';
2015-06-11 wenzelm 2015-06-11 support for 'consider' command; allow full "fixes" for 'obtain' command; tuned signature;
2015-06-05 wenzelm 2015-06-05 added Isar command 'supply';
2015-05-30 wenzelm 2015-05-30 unused;
2015-04-16 wenzelm 2015-04-16 clarified thy_deps;
2015-04-09 wenzelm 2015-04-09 clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
2015-04-06 wenzelm 2015-04-06 support for 'restricted' modifier: only qualified accesses outside the local scope;
2015-04-04 wenzelm 2015-04-04 support private scope for individual local theory commands; tuned signature;
2015-04-01 wenzelm 2015-04-01 added command 'experiment';
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-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-06 wenzelm 2014-11-06 simplified keyword kinds; more explicit bootstrap syntax;
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 eliminated spurious semicolons;
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-31 wenzelm 2014-10-31 discontinued Proof General;
2014-10-28 wenzelm 2014-10-28 explicit keyword category for commands that may start a block;
2014-10-13 wenzelm 2014-10-13 clarified load order; tuned signature;
2014-10-13 wenzelm 2014-10-13 support for named plugins for definitional packages;
2014-10-07 wenzelm 2014-10-07 more symbols;
2014-10-07 wenzelm 2014-10-07 more cartouches;
2014-10-05 wenzelm 2014-10-05 bibtex support in ML: document antiquotation @{cite} with markup;
2014-09-07 haftmann 2014-09-07 separated class_deps command into separate file
2014-08-14 wenzelm 2014-08-14 tuned signature -- prefer self-contained user-space tool;
2014-08-10 wenzelm 2014-08-10 support for named collections of theorems in canonical order;
2014-07-04 wenzelm 2014-07-04 suppress completion of obscure keyword;
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-05-05 wenzelm 2014-05-05 support print operations as asynchronous query;
2014-04-29 wenzelm 2014-04-29 suppress slightly odd completions of "real";