| Thu, 11 Jun 2015 22:47:53 +0200 |
wenzelm |
support for 'consider' command;
|
file |
diff |
annotate
|
| Fri, 05 Jun 2015 13:41:06 +0200 |
wenzelm |
added Isar command 'supply';
|
file |
diff |
annotate
|
| Sat, 30 May 2015 22:18:12 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 13:48:10 +0200 |
wenzelm |
clarified thy_deps;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 22:11:01 +0200 |
wenzelm |
support for 'restricted' modifier: only qualified accesses outside the local scope;
|
file |
diff |
annotate
|
| Sat, 04 Apr 2015 14:04:11 +0200 |
wenzelm |
support private scope for individual local theory commands;
|
file |
diff |
annotate
|
| Wed, 01 Apr 2015 22:08:06 +0200 |
wenzelm |
added command 'experiment';
|
file |
diff |
annotate
|
| Thu, 13 Nov 2014 23:45:15 +0100 |
wenzelm |
uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 16:36:55 +0100 |
wenzelm |
plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
|
file |
diff |
annotate
|
| Thu, 06 Nov 2014 11:44:41 +0100 |
wenzelm |
simplified keyword kinds;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 15:27:37 +0100 |
wenzelm |
uniform heading commands work in any context, even in theory header;
|
file |
diff |
annotate
|
| Sat, 01 Nov 2014 14:20:38 +0100 |
wenzelm |
eliminated spurious semicolons;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 16:03:45 +0100 |
wenzelm |
discontinued Isar TTY loop;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 15:15:10 +0100 |
wenzelm |
removed obsolete Proof General commands;
|
file |
diff |
annotate
|
| Fri, 31 Oct 2014 11:18:17 +0100 |
wenzelm |
discontinued Proof General;
|
file |
diff |
annotate
|
| Tue, 28 Oct 2014 11:42:51 +0100 |
wenzelm |
explicit keyword category for commands that may start a block;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 19:34:10 +0200 |
wenzelm |
clarified load order;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 15:45:23 +0200 |
wenzelm |
support for named plugins for definitional packages;
|
file |
diff |
annotate
|
| Tue, 07 Oct 2014 20:34:17 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 07 Oct 2014 20:27:31 +0200 |
wenzelm |
more cartouches;
|
file |
diff |
annotate
|
| Sun, 05 Oct 2014 16:05:17 +0200 |
wenzelm |
bibtex support in ML: document antiquotation @{cite} with markup;
|
file |
diff |
annotate
|
| Sun, 07 Sep 2014 17:51:28 +0200 |
haftmann |
separated class_deps command into separate file
|
file |
diff |
annotate
|
| Thu, 14 Aug 2014 10:48:40 +0200 |
wenzelm |
tuned signature -- prefer self-contained user-space tool;
|
file |
diff |
annotate
|
| Sun, 10 Aug 2014 16:13:12 +0200 |
wenzelm |
support for named collections of theorems in canonical order;
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 15:46:13 +0200 |
wenzelm |
suppress completion of obscure keyword;
|
file |
diff |
annotate
|
| Mon, 30 Jun 2014 10:34:28 +0200 |
wenzelm |
removed obsolete Isar system commands -- raw ML console is normally used for system tinkering;
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 16:04:56 +0200 |
wenzelm |
command 'print_term_bindings' supersedes 'print_binds';
|
file |
diff |
annotate
|
| Mon, 05 May 2014 15:17:07 +0200 |
wenzelm |
support print operations as asynchronous query;
|
file |
diff |
annotate
|
| Tue, 29 Apr 2014 22:52:15 +0200 |
wenzelm |
suppress slightly odd completions of "real";
|
file |
diff |
annotate
|
| Sat, 19 Apr 2014 17:23:05 +0200 |
wenzelm |
added command 'SML_export' and 'SML_import' for exchange of toplevel bindings;
|
file |
diff |
annotate
|
| Tue, 25 Mar 2014 13:18:10 +0100 |
wenzelm |
added command 'SML_file' for Standard ML without Isabelle/ML add-ons;
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 16:16:28 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 12 Mar 2014 21:58:48 +0100 |
wenzelm |
simplified programming interface to define ML antiquotations -- NB: the transformed context ignores updates of the context parser;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 10:45:06 +0100 |
wenzelm |
suppress completion of obscure keyword, avoid confusion with plain "simp";
|
file |
diff |
annotate
|
| Sun, 16 Feb 2014 17:25:03 +0100 |
wenzelm |
prefer user-space tool within Pure.thy;
|
file |
diff |
annotate
|
| Mon, 10 Feb 2014 22:08:18 +0100 |
wenzelm |
discontinued axiomatic 'classes', 'classrel', 'arities';
|
file |
diff |
annotate
|
| Sun, 26 Jan 2014 14:01:19 +0100 |
wenzelm |
discontinued obsolete attribute "standard";
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 18:34:05 +0100 |
wenzelm |
prefer self-contained user-space tool;
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 18:18:03 +0100 |
wenzelm |
define basic attributes in user-space Pure.thy -- which provides better hyperlinks and may serve as example;
|
file |
diff |
annotate
|
| Fri, 17 Jan 2014 20:31:39 +0100 |
wenzelm |
prefer user-space tool within Pure.thy;
|
file |
diff |
annotate
|
| Thu, 12 Dec 2013 21:28:13 +0100 |
wenzelm |
skeleton for Simplifier trace by Lars Hupel;
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 11:08:28 +0200 |
wenzelm |
moved module into plain Isabelle/ML user space;
|
file |
diff |
annotate
|
| Wed, 11 Sep 2013 20:16:28 +0200 |
wenzelm |
more explicit indication of 'done' as proof script element;
|
file |
diff |
annotate
|
| Mon, 02 Sep 2013 16:10:26 +0200 |
wenzelm |
more explicit indication of 'guess' as improper Isar (aka "script") element;
|
file |
diff |
annotate
|
| Sun, 07 Jul 2013 18:34:29 +0200 |
wenzelm |
discontinued command 'print_drafts';
|
file |
diff |
annotate
|
| Tue, 25 Jun 2013 20:35:50 +0200 |
wenzelm |
recover command tags from 4cf3f6153eb8 -- important for document preparation;
|
file |
diff |
annotate
|
| Mon, 24 Jun 2013 23:33:14 +0200 |
wenzelm |
improved "isabelle keywords" and "isabelle update_keywords" based on Isabelle/Scala, without requiring to build sessions first;
|
file |
diff |
annotate
|
| Mon, 24 Jun 2013 17:17:17 +0200 |
wenzelm |
back to keyword 'pr' :: diag as required for ProofGeneral command line -- reject this TTY command in Isabelle/jEdit by other means;
|
file |
diff |
annotate
|
| Mon, 24 Jun 2013 17:03:53 +0200 |
wenzelm |
more formal ProofGeneral command setup within theory Pure;
|
file |
diff |
annotate
|
| Sun, 23 Jun 2013 21:23:36 +0200 |
wenzelm |
proper diagnostic command 'print_state';
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:37:53 +0200 |
wenzelm |
syntax translations always depend on context;
|
file |
diff |
annotate
|
| Fri, 17 May 2013 20:53:28 +0200 |
wenzelm |
renamed 'print_configs' to 'print_options';
|
file |
diff |
annotate
|
| Wed, 15 May 2013 20:34:42 +0200 |
wenzelm |
moved files;
|
file |
diff |
annotate
|
| Wed, 15 May 2013 20:22:46 +0200 |
wenzelm |
maintain ProofGeneral preferences within ProofGeneral module;
|
file |
diff |
annotate
|
| Sat, 30 Mar 2013 14:57:06 +0100 |
wenzelm |
added 'print_defn_rules' command;
|
file |
diff |
annotate
|
| Thu, 28 Feb 2013 16:38:17 +0100 |
wenzelm |
discontinued obsolete 'axioms' command;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2013 17:32:17 +0100 |
wenzelm |
discontinued redundant 'use' command;
|
file |
diff |
annotate
|
| Wed, 27 Feb 2013 12:45:19 +0100 |
wenzelm |
discontinued obsolete 'uses' within theory header;
|
file |
diff |
annotate
|
| Mon, 25 Feb 2013 13:29:19 +0100 |
wenzelm |
discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
|
file |
diff |
annotate
|