src/Pure/Pure.thy
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;
Mon, 22 Jun 2015 20:36:33 +0200 wenzelm support 'when' statement, which corresponds to 'presume';
Thu, 11 Jun 2015 22:47:53 +0200 wenzelm support for 'consider' command;
Fri, 05 Jun 2015 13:41:06 +0200 wenzelm added Isar command 'supply';
Sat, 30 May 2015 22:18:12 +0200 wenzelm unused;
Thu, 16 Apr 2015 13:48:10 +0200 wenzelm clarified thy_deps;
Thu, 09 Apr 2015 20:42:32 +0200 wenzelm clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
Mon, 06 Apr 2015 22:11:01 +0200 wenzelm support for 'restricted' modifier: only qualified accesses outside the local scope;
Sat, 04 Apr 2015 14:04:11 +0200 wenzelm support private scope for individual local theory commands;
Wed, 01 Apr 2015 22:08:06 +0200 wenzelm added command 'experiment';
Thu, 13 Nov 2014 23:45:15 +0100 wenzelm uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
less more (0) -100 -60 tip