Tue, 17 Oct 2023 22:25:48 +0200 |
wenzelm |
clarified 'simproc_setup';
|
file |
diff |
annotate
|
Sun, 12 Sep 2021 22:31:51 +0200 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
Fri, 08 Apr 2016 20:15:20 +0200 |
wenzelm |
eliminated unused simproc identifier;
|
file |
diff |
annotate
|
Wed, 09 Sep 2015 20:57:21 +0200 |
wenzelm |
simplified simproc programming interfaces;
|
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
|
Fri, 06 Mar 2015 23:57:01 +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, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
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
|
Mon, 09 Jan 2012 18:29:42 +0100 |
wenzelm |
prefer antiquotations;
|
file |
diff |
annotate
|
Mon, 08 Aug 2011 18:36:32 -0700 |
huffman |
HOLCF: fix warnings about unreferenced identifiers
|
file |
diff |
annotate
|
Fri, 13 May 2011 23:58:40 +0200 |
wenzelm |
clarified map_simpset versus Simplifier.map_simpset_global;
|
file |
diff |
annotate
|
Tue, 29 Mar 2011 17:47:11 +0200 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
Thu, 24 Mar 2011 16:56:19 +0100 |
wenzelm |
added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
|
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
|