src/Pure/Pure.thy
Tue, 26 Nov 2019 08:09:44 +0100 ballarin Remove diagnostic command 'print_dependencies'.
Fri, 23 Aug 2019 14:32:51 +0200 wenzelm clarified 'thm_deps' command;
Sat, 17 Aug 2019 19:04:03 +0200 wenzelm clarified signature;
Sat, 17 Aug 2019 12:44:22 +0200 wenzelm added command 'thm_oracles';
Sun, 28 Apr 2019 13:09:15 +0200 wenzelm tuned signature;
Wed, 17 Apr 2019 16:57:06 +0000 haftmann backed out experimental b67bab2b132c, which slipped in accidentally
Tue, 16 Apr 2019 19:50:30 +0000 haftmann hierarchically inclusive named theorem collections
Sat, 13 Apr 2019 13:30:02 +0200 wenzelm more abbrevs;
Thu, 04 Apr 2019 22:17:37 +0200 wenzelm tuned;
Thu, 04 Apr 2019 20:45:55 +0200 wenzelm type Path.binding may be empty: check later via proper_binding;
Thu, 04 Apr 2019 16:47:09 +0200 wenzelm clarified export_files: Isabelle_System.copy_file_base preserves given directory sub-structure;
Thu, 04 Apr 2019 14:30:58 +0200 wenzelm added command 'compile_generated_files';
Wed, 03 Apr 2019 21:50:00 +0200 wenzelm clarified signature: more explicit operations for corresponding Isar commands;
Thu, 28 Mar 2019 21:24:55 +0100 wenzelm "export_code ... file_prefix ..." is the preferred way to produce output within the logical file-system within the theory context, as well as session exports;
Thu, 14 Mar 2019 16:55:06 +0100 wenzelm more specific keyword kinds;
Sun, 10 Mar 2019 21:12:29 +0100 wenzelm document markers are formal comments, and may thus occur anywhere in the command-span;
Sun, 10 Mar 2019 00:21:34 +0100 wenzelm added semantic document markers;
Tue, 15 Jan 2019 20:03:53 +0100 wenzelm added command 'export_generated_files';
Thu, 20 Dec 2018 12:40:24 +0000 haftmann disregard historic keyword
Sat, 01 Dec 2018 16:11:59 +0100 wenzelm clarified modules;
Fri, 30 Nov 2018 23:43:10 +0100 wenzelm more general command 'generate_file' for registered file types, notably Haskell;
Tue, 27 Nov 2018 21:07:39 +0100 wenzelm more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
Thu, 08 Nov 2018 13:42:36 +0100 wenzelm more standard Resources.provide_parse_files: avoid duplicate markup reports;
Mon, 24 Sep 2018 19:53:45 +0200 wenzelm tuned signature: prefer value-oriented pretty-printing;
Mon, 24 Sep 2018 19:34:14 +0200 wenzelm tuned signature: prefer value-oriented pretty-printing;
Sun, 02 Sep 2018 14:14:43 +0200 wenzelm no reset_proof for notepad: begin/end structure takes precedence over goal/proof structure;
Tue, 28 Aug 2018 11:22:04 +0200 wenzelm tuned signature;
Tue, 28 Aug 2018 11:13:33 +0200 wenzelm clarified ML_environment: ML_write_global requires "Isabelle";
Mon, 27 Aug 2018 17:30:13 +0200 wenzelm clarified environment: allow "read>write" specification;
Mon, 27 Aug 2018 14:42:24 +0200 wenzelm support named ML environments, notably "Isabelle", "SML";
Sun, 26 Aug 2018 17:28:38 +0200 wenzelm clarified signature;
Tue, 26 Jun 2018 14:01:46 +0200 wenzelm clarified default tag;
Thu, 21 Jun 2018 14:49:21 +0200 wenzelm clarified signature;
Fri, 25 May 2018 22:47:57 +0200 wenzelm added command 'ML_export';
Tue, 06 Mar 2018 22:59:00 +0100 ballarin Drop rewrite rule arguments of sublocale and interpretation implementations.
Sun, 04 Mar 2018 12:22:48 +0100 ballarin Drop rewrites after defines in interpretations.
Fri, 02 Mar 2018 14:19:25 +0100 ballarin Proper rewrite morphisms in locale instances.
Sun, 25 Feb 2018 19:30:55 +0100 wenzelm tuned;
Tue, 16 Jan 2018 19:28:05 +0100 ballarin Experimental support for rewrite morphisms in locale instances.
Tue, 16 Jan 2018 11:27:52 +0100 wenzelm discontinued old form of marginal comments;
Tue, 09 Jan 2018 15:40:12 +0100 wenzelm clarified modules;
Thu, 28 Dec 2017 12:07:52 +0100 wenzelm prefer existing Resources.check_path;
Thu, 28 Dec 2017 11:49:54 +0100 wenzelm added command 'bibtex_file' (for PIDE interaction only);
Fri, 22 Dec 2017 18:32:59 +0100 wenzelm discontinued 'display_drafts' command;
Wed, 06 Dec 2017 18:59:33 +0100 wenzelm prefer control symbol antiquotations;
Sun, 03 Dec 2017 13:22:09 +0100 wenzelm discontinued old 'def' command;
Wed, 29 Nov 2017 10:27:56 +0100 wenzelm clarified dependencies: "isabelle build -S" should be invariant wrt. change of ML system or platform;
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;
less more (0) -100 -60 tip