| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Mon, 02 Dec 2019 15:04:38 +0100 |
wenzelm |
proper spec_rule name via naming/binding/Morphism.binding;
|
file |
diff |
annotate
|
| Fri, 29 Nov 2019 20:57:04 +0100 |
wenzelm |
more informative spec rules: optional name;
|
file |
diff |
annotate
|
| Tue, 04 Jun 2019 15:11:29 +0200 |
wenzelm |
proper Proof_Context.export_morphism corresponding to Proof_Context.augment (see 7f568724d67e);
|
file |
diff |
annotate
|
| Mon, 03 Jun 2019 15:40:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 21 Feb 2019 09:15:07 +0000 |
haftmann |
streamlined specification interfaces
|
file |
diff |
annotate
|
| Mon, 21 Jan 2019 07:08:55 +0000 |
haftmann |
slightly more conventional naming schema
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Tue, 06 Mar 2018 14:41:05 +0100 |
wenzelm |
eliminated dead code from 2a1acc88a180 (presumably left over from ML type-inference experimentation);
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 19:25:37 +0100 |
wenzelm |
added HOLogic.mk_obj_eq convenience and eliminated some clones;
|
file |
diff |
annotate
|
| Mon, 19 Feb 2018 14:49:11 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 18 Feb 2018 15:05:21 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 16 Feb 2018 22:11:59 +0100 |
wenzelm |
trim context of persistent data;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2017 21:08:32 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 05 Apr 2017 19:23:41 +0200 |
Lars Hupel |
use Item_Net to store inductive info
|
file |
diff |
annotate
|
| Tue, 13 Sep 2016 20:51:14 +0200 |
traytel |
don't expose internal construction in the coinduction rule for mutual coinductive predicates
|
file |
diff |
annotate
|
| Tue, 05 Jul 2016 14:20:27 +0200 |
wenzelm |
PIDE reports of implicit variable scope;
|
file |
diff |
annotate
|
| Sat, 11 Jun 2016 16:41:11 +0200 |
wenzelm |
clarified syntax;
|
file |
diff |
annotate
|
| Sun, 29 May 2016 15:40:25 +0200 |
wenzelm |
clarified check_open_spec / read_open_spec;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 09:43:11 +0200 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 20:24:19 +0200 |
wenzelm |
prefer internal attribute source;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2016 22:38:50 +0200 |
wenzelm |
clarified bindings;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 15:53:39 +0100 |
wenzelm |
more uniform treatment of package internals;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 16:34:26 +0100 |
wenzelm |
clarified position information;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 16:13:15 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 15 Nov 2015 12:39:51 +0100 |
wenzelm |
option "inductive_defs" controls exposure of def and mono facts;
|
file |
diff |
annotate
|
| Fri, 02 Oct 2015 19:34:12 +0200 |
wenzelm |
avoid useless empty case_names;
|
file |
diff |
annotate
|
| Fri, 25 Sep 2015 20:37:59 +0200 |
wenzelm |
moved remaining display.ML to more_thm.ML;
|
file |
diff |
annotate
|
| Mon, 31 Aug 2015 19:02:00 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Sun, 26 Jul 2015 17:24:54 +0200 |
wenzelm |
updated to infer_instantiate;
|
file |
diff |
annotate
|
| Tue, 02 Jun 2015 11:03:02 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Thu, 16 Apr 2015 15:22:44 +0200 |
wenzelm |
discontinued pointless warnings: commands are only defined inside a theory context;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 23:14:05 +0200 |
wenzelm |
local setup of induction tools, with restricted access to auxiliary consts;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
file |
diff |
annotate
|
| Fri, 03 Apr 2015 19:56:51 +0200 |
wenzelm |
more uniform "verbose" option to print name space;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 17:34:52 +0200 |
wenzelm |
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 29 Mar 2015 21:47:16 +0200 |
wenzelm |
ind_cases: clarified preparation of arguments;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:56:43 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 03 Mar 2015 19:08:04 +0100 |
traytel |
eliminated some clones of Proof_Context.cterm_of
|
file |
diff |
annotate
|
| Wed, 11 Feb 2015 11:42:39 +0100 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 16:46:21 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 15:46:19 +0100 |
haftmann |
do not conceal inductive predicate names properly, following 4a3747517552
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 15:46:17 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 12 Nov 2014 18:18:38 +0100 |
wenzelm |
prefer independent parallel map where user input is processed -- avoid non-deterministic feedback in error situations;
|
file |
diff |
annotate
|
| Mon, 10 Nov 2014 21:49:48 +0100 |
wenzelm |
proper context for assume_tac (atac remains as fall-back without context);
|
file |
diff |
annotate
|
| Fri, 07 Nov 2014 22:15:51 +0100 |
wenzelm |
eliminated pointless check -- command definitions are subject to theory context;
|
file |
diff |
annotate
|
| Mon, 03 Nov 2014 14:50:27 +0100 |
wenzelm |
eliminated unused int_only flag (see also c12484a27367);
|
file |
diff |
annotate
|
| Thu, 30 Oct 2014 22:45:19 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 11:41:54 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Thu, 21 Aug 2014 22:48:39 +0200 |
wenzelm |
tuned signature -- define some elementary operations earlier;
|
file |
diff |
annotate
|
| Tue, 19 Aug 2014 23:17:51 +0200 |
wenzelm |
tuned signature -- moved type src to Token, without aliases;
|
file |
diff |
annotate
|
| Mon, 31 Mar 2014 12:35:39 +0200 |
wenzelm |
some shortcuts for chunks, which sometimes avoid bulky string output;
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 15:58:27 +0100 |
wenzelm |
avoid hard-wired theory names;
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|