| Fri, 15 Oct 2021 22:00:28 +0200 |
wenzelm |
revert bbfed17243af, breaks HOL-Proofs extraction;
|
file |
diff |
annotate
|
| Fri, 15 Oct 2021 20:54:13 +0200 |
wenzelm |
proper context for Goal.prove_internal;
|
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
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 14:30:24 +0200 |
wenzelm |
clarified bindings;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2016 22:10:09 +0200 |
wenzelm |
clarified bindings;
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 15:53:39 +0100 |
wenzelm |
more uniform treatment of package internals;
|
file |
diff |
annotate
|
| Sun, 06 Sep 2015 21:55:13 +0200 |
wenzelm |
do not expose low-level "_def" facts of 'function' definitions, to avoid potential confusion with the situation of plain 'definition';
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 13:35:16 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 20:08:45 +0100 |
wenzelm |
proper 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
|
| Fri, 06 Mar 2015 13:39:34 +0100 |
wenzelm |
clarified 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, 30 Oct 2014 22:45:19 +0100 |
wenzelm |
eliminated aliases;
|
file |
diff |
annotate
|
| Wed, 08 Oct 2014 17:09:07 +0200 |
wenzelm |
added parameterized ML antiquotations @{map N}, @{fold N}, @{fold_map N}, @{split_list N};
|
file |
diff |
annotate
|
| Fri, 21 Mar 2014 20:33:56 +0100 |
wenzelm |
more qualified names;
|
file |
diff |
annotate
|
| Tue, 31 Dec 2013 14:29:16 +0100 |
wenzelm |
proper context for norm_hhf and derived operations;
|
file |
diff |
annotate
|
| Sat, 14 Dec 2013 17:28:05 +0100 |
wenzelm |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 14:24:34 +0100 |
blanchet |
ported part of function package to new 'Ctr_Sugar' abstraction
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 14:00:56 +0100 |
blanchet |
undid copy-paste
|
file |
diff |
annotate
|
| Sun, 16 Oct 2011 18:48:30 +0200 |
wenzelm |
added Term.dummy_pattern conveniences;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 23:04:28 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 21:17:47 +0200 |
krauss |
inlined Function_Lib.replace_frees, which is used only once
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 21:50:04 +0200 |
wenzelm |
clarified Variable.focus vs. Variable.focus_cterm -- eliminated clone;
|
file |
diff |
annotate
|
| Wed, 27 Apr 2011 10:49:39 +0200 |
wenzelm |
eliminated obsolete Function_Lib.frees_in_term;
|
file |
diff |
annotate
|
| Mon, 13 Dec 2010 10:15:27 +0100 |
krauss |
eliminated dest_all_all_ctx
|
file |
diff |
annotate
|
| Mon, 13 Dec 2010 10:15:26 +0100 |
krauss |
private term variant of Variable.focus
|
file |
diff |
annotate
|
| Sun, 12 Dec 2010 21:40:59 +0100 |
krauss |
added signature;
|
file |
diff |
annotate
|
| Fri, 26 Nov 2010 22:29:41 +0100 |
wenzelm |
make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;
|
file |
diff |
annotate
|
| Fri, 22 Oct 2010 23:45:20 +0200 |
krauss |
some cleanup in Function_Lib
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 12:34:41 +0200 |
krauss |
consolidated tupled_lambda; moved to structure HOLogic
|
file |
diff |
annotate
|
| Thu, 08 Jul 2010 16:19:24 +0200 |
haftmann |
tuned titles
|
file |
diff |
annotate
|
| Thu, 10 Jun 2010 12:24:03 +0200 |
haftmann |
tuned quotes, antiquotations and whitespace
|
file |
diff |
annotate
|
| Sat, 15 May 2010 21:50:05 +0200 |
wenzelm |
less pervasive names from structure Thm;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2010 20:57:08 +0100 |
wenzelm |
clarified @{const_name} vs. @{const_abbrev};
|
file |
diff |
annotate
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
new year's resolution: reindented code in function package
|
file |
diff |
annotate
|
| Mon, 23 Nov 2009 15:05:59 +0100 |
krauss |
eliminated dead code and some unused bindings, reported by polyml
|
file |
diff |
annotate
|
| Wed, 11 Nov 2009 10:06:30 +0100 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Fri, 23 Oct 2009 16:22:10 +0200 |
krauss |
function package: more standard names for structures and files
|
file |
diff |
annotate
|