src/Pure/Pure.thy
18 months ago wenzelm 2017-12-03 discontinued old 'def' command;
18 months ago wenzelm 2017-11-29 clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform;
19 months ago wenzelm 2017-11-08 formal dependency on "poly" executable;
19 months ago wenzelm 2017-11-05 more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
20 months ago wenzelm 2017-10-02 added command 'external_file';
23 months ago haftmann 2017-07-02 proper concept of code declaration wrt. atomicity and Isar declarations
23 months ago wenzelm 2017-07-03 added command 'alias' and 'type_alias';
24 months ago wenzelm 2017-06-26 clarified indentation;
2016-12-28 wenzelm 2016-12-28 more uniform treatment of "bad" like other messages (with serial number);
2016-12-18 wenzelm 2016-12-18 tuned;
2016-09-14 wenzelm 2016-09-14 discontinued global etc/abbrevs;
2016-09-06 wenzelm 2016-09-06 strictly sequential abbrevs;
2016-08-02 wenzelm 2016-08-02 support 'abbrevs' within theory header; simplified 'keywords': no abbreviations here;
2016-07-16 wenzelm 2016-07-16 information about proof outline with cases (sendback);
2016-07-15 wenzelm 2016-07-15 singleton result for 'proof' command (without backtracking), e.g. relevant for well-defined output;
2016-07-11 wenzelm 2016-07-11 clarified indentation;
2016-07-11 wenzelm 2016-07-11 explicit kind "before_command"; tuned signature;
2016-07-11 wenzelm 2016-07-11 more indentation for quasi_command keywords;
2016-06-23 wenzelm 2016-06-23 tuned signature;
2016-06-21 wenzelm 2016-06-21 tuned;
2016-06-11 wenzelm 2016-06-11 clarified syntax;
2016-06-10 wenzelm 2016-06-10 added command 'unbundle';
2016-06-10 wenzelm 2016-06-10 prefer hybrid 'bundle' command;
2016-06-09 wenzelm 2016-06-09 clarified;
2016-06-09 wenzelm 2016-06-09 support for bundle definition via target;
2016-05-29 wenzelm 2016-05-29 clarified check_open_spec / read_open_spec; allow 'for' fixes in 'abbreviation', 'definition';
2016-05-28 wenzelm 2016-05-28 clarified 'axiomatization';
2016-05-14 wenzelm 2016-05-14 toplevel theorem statements support 'if'/'for' eigen-context;
2016-04-28 wenzelm 2016-04-28 support 'assumes' in specifications, e.g. 'definition', 'inductive'; tuned signatures;
2016-04-26 wenzelm 2016-04-26 'obtain' supports structured statements (similar to 'define');
2016-04-25 wenzelm 2016-04-25 old 'def' is legacy;
2016-04-24 wenzelm 2016-04-24 added Isar command 'define';
2016-04-13 wenzelm 2016-04-13 eliminated "xname" and variants;
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;