| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Fri, 15 Oct 2021 19:25:31 +0200 |
wenzelm |
discontinued Term.dest_abs / Logic.dest_all, which are officially superseded by Variable.dest_abs etc., but there are also Term.dest_abs_global to recover existing tools easily;
|
file |
diff |
annotate
|
| Sun, 12 Sep 2021 22:31:51 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 11 Jun 2016 16:41:11 +0200 |
wenzelm |
clarified syntax;
|
file |
diff |
annotate
|
| Mon, 30 May 2016 14:15:44 +0200 |
wenzelm |
allow 'for' fixes for multi_specs;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 09:43:11 +0200 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:54:56 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Mon, 06 Apr 2015 17:06:48 +0200 |
wenzelm |
@{command_spec} is superseded by @{command_keyword};
|
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
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 17:04:14 +0100 |
wenzelm |
proper context for match_tac etc.;
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 16:18:39 +0200 |
wenzelm |
clarified order of rules for match_tac/resolve_tac;
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 11:35:33 +0200 |
wenzelm |
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Thu, 12 Apr 2012 18:39:19 +0200 |
wenzelm |
more standard method setup;
|
file |
diff |
annotate
|
| Fri, 23 Mar 2012 20:32:43 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 18:20:12 +0100 |
wenzelm |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 20:07:00 +0100 |
wenzelm |
prefer formally checked @{keyword} parser;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 20:04:24 +0100 |
wenzelm |
more explicit indication of def names;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 11:22:39 +0100 |
wenzelm |
tuned strip_alls;
|
file |
diff |
annotate
|
| Fri, 16 Dec 2011 10:52:35 +0100 |
wenzelm |
clarified modules that contribute to datatype package;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2011 13:25:54 +0100 |
huffman |
more error checking for fixrec
|
file |
diff |
annotate
|
| Sat, 19 Nov 2011 21:18:38 +0100 |
wenzelm |
added ML antiquotation @{attributes};
|
file |
diff |
annotate
|
| Mon, 08 Aug 2011 18:36:32 -0700 |
huffman |
HOLCF: fix warnings about unreferenced identifiers
|
file |
diff |
annotate
|
| Thu, 09 Jun 2011 16:34:49 +0200 |
wenzelm |
discontinued Name.variant to emphasize that this is old-style / indirect;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Tue, 29 Mar 2011 17:47:11 +0200 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Sun, 19 Dec 2010 18:15:21 -0800 |
huffman |
switch to transparent ascription, to avoid warning messages
|
file |
diff |
annotate
|
| Tue, 30 Nov 2010 14:21:57 -0800 |
huffman |
remove gratuitous semicolons from ML code
|
file |
diff |
annotate
|
| Sat, 27 Nov 2010 16:08:10 -0800 |
huffman |
moved directory src/HOLCF to src/HOL/HOLCF;
|
file |
diff |
annotate
| base
|