src/Pure/Pure.thy
Wed, 08 Nov 2017 17:34:32 +0100 wenzelm formal dependency on "poly" executable;
Sun, 05 Nov 2017 17:45:17 +0100 wenzelm more uniform header syntax, in contrast to the former etc/abbrevs file-format (see 73939a9b70a3);
Mon, 02 Oct 2017 19:28:18 +0200 wenzelm added command 'external_file';
Sun, 02 Jul 2017 20:13:38 +0200 haftmann proper concept of code declaration wrt. atomicity and Isar declarations
Mon, 03 Jul 2017 13:51:55 +0200 wenzelm added command 'alias' and 'type_alias';
Mon, 26 Jun 2017 11:07:48 +0200 wenzelm clarified indentation;
Wed, 28 Dec 2016 10:39:50 +0100 wenzelm more uniform treatment of "bad" like other messages (with serial number);
Sun, 18 Dec 2016 12:34:31 +0100 wenzelm tuned;
Wed, 14 Sep 2016 14:37:38 +0200 wenzelm discontinued global etc/abbrevs;
Tue, 06 Sep 2016 13:26:14 +0200 wenzelm strictly sequential abbrevs;
Tue, 02 Aug 2016 17:35:18 +0200 wenzelm support 'abbrevs' within theory header;
Sat, 16 Jul 2016 00:38:33 +0200 wenzelm information about proof outline with cases (sendback);
Fri, 15 Jul 2016 23:46:28 +0200 wenzelm singleton result for 'proof' command (without backtracking), e.g. relevant for well-defined output;
Mon, 11 Jul 2016 20:58:00 +0200 wenzelm clarified indentation;
Mon, 11 Jul 2016 16:36:29 +0200 wenzelm explicit kind "before_command";
Mon, 11 Jul 2016 10:43:54 +0200 wenzelm more indentation for quasi_command keywords;
Thu, 23 Jun 2016 11:01:14 +0200 wenzelm tuned signature;
Tue, 21 Jun 2016 17:35:45 +0200 wenzelm tuned;
Sat, 11 Jun 2016 16:41:11 +0200 wenzelm clarified syntax;
Fri, 10 Jun 2016 22:47:25 +0200 wenzelm added command 'unbundle';
Fri, 10 Jun 2016 12:45:34 +0200 wenzelm prefer hybrid 'bundle' command;
Thu, 09 Jun 2016 17:13:52 +0200 wenzelm clarified;
Thu, 09 Jun 2016 15:41:49 +0200 wenzelm support for bundle definition via target;
Sun, 29 May 2016 15:40:25 +0200 wenzelm clarified check_open_spec / read_open_spec;
Sat, 28 May 2016 21:38:58 +0200 wenzelm clarified 'axiomatization';
Sat, 14 May 2016 19:49:10 +0200 wenzelm toplevel theorem statements support 'if'/'for' eigen-context;
Thu, 28 Apr 2016 09:43:11 +0200 wenzelm support 'assumes' in specifications, e.g. 'definition', 'inductive';
Tue, 26 Apr 2016 22:39:17 +0200 wenzelm 'obtain' supports structured statements (similar to 'define');
Mon, 25 Apr 2016 19:41:39 +0200 wenzelm old 'def' is legacy;
Sun, 24 Apr 2016 21:31:14 +0200 wenzelm added Isar command 'define';
Wed, 13 Apr 2016 18:01:05 +0200 wenzelm eliminated "xname" and variants;
Sun, 10 Apr 2016 21:46:12 +0200 wenzelm more standard session build process, including browser_info;
Fri, 08 Apr 2016 20:15:20 +0200 wenzelm eliminated unused simproc identifier;
Thu, 07 Apr 2016 16:53:43 +0200 wenzelm more conventional theory syntax for ML bootstrap, with 'ML_file' instead of 'use';
Thu, 07 Apr 2016 12:13:11 +0200 wenzelm Pure attribute setup is back to Pure/Isar/attrib.ML, where it can be editing continuously (see also 7eb0c04e4c40);
Tue, 05 Apr 2016 18:20:25 +0200 wenzelm support bootstrap from fresh SML environment, with syntax of Isabelle/ML or SML;
Tue, 05 Apr 2016 15:53:48 +0200 wenzelm tuned;
Mon, 04 Apr 2016 23:58:48 +0200 wenzelm more uniform ML file commands;
Mon, 04 Apr 2016 23:08:43 +0200 wenzelm tuned whitespace;
Mon, 04 Apr 2016 22:13:08 +0200 wenzelm tuned -- more explicit sections;
Mon, 04 Apr 2016 17:25:53 +0200 wenzelm clarified bootstrap -- avoid 'ML_file' in Pure.thy for uniformity;
Mon, 04 Apr 2016 17:02:34 +0200 wenzelm clarified bootstrap -- more uniform use of ML files;
Tue, 01 Mar 2016 19:42:59 +0100 wenzelm ML debugger support in Pure (again, see 3565c9f407ec);
Sun, 14 Feb 2016 16:30:27 +0100 wenzelm command '\<proof>' is an alias for 'sorry', with different typesetting;
Wed, 13 Jan 2016 16:55:56 +0100 wenzelm removed old 'defs' command;
Sat, 19 Dec 2015 11:05:04 +0100 haftmann abandoned attempt to unify sublocale and interpretation into global theories
Wed, 16 Dec 2015 16:31:36 +0100 wenzelm rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
Sat, 14 Nov 2015 08:45:52 +0100 haftmann prefer "rewrites" and "defines" to note rewrite morphisms
Sat, 14 Nov 2015 08:45:52 +0100 haftmann coalesce permanent_interpretation.ML with interpretation.ML
Tue, 10 Nov 2015 20:10:17 +0100 wenzelm clarified modules;
Thu, 05 Nov 2015 00:02:30 +0100 wenzelm symbolic syntax "\<comment> text";
Wed, 04 Nov 2015 08:13:52 +0100 ballarin Keyword 'rewrites' identifies rewrite morphisms.
Tue, 06 Oct 2015 15:39:00 +0200 wenzelm added 'proposition' command;
Tue, 06 Oct 2015 15:14:28 +0200 wenzelm fewer aliases for toplevel theorem statements;
Tue, 22 Sep 2015 18:56:25 +0200 wenzelm separate command 'print_definitions';
Mon, 17 Aug 2015 19:34:15 +0200 wenzelm support for ML files with/without debugger information;
Fri, 17 Jul 2015 21:40:47 +0200 wenzelm skeleton for interactive debugger;
Wed, 08 Jul 2015 15:37:32 +0200 wenzelm clarified text folds: proof ... qed counts as extra block;
Wed, 01 Jul 2015 21:48:46 +0200 wenzelm clarified keyword categories;
Wed, 01 Jul 2015 21:29:57 +0200 wenzelm support for subgoal focus command;
less more (0) -100 -60 tip