| Wed, 07 Aug 2019 10:42:34 +0200 |
wenzelm |
more careful treatment of implicit context;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Fri, 27 May 2016 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 14:47:27 +0200 |
wenzelm |
clarified bindings;
|
file |
diff |
annotate
|
| Mon, 18 Apr 2016 14:30:24 +0200 |
wenzelm |
clarified bindings;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2016 20:54:17 +0200 |
wenzelm |
prefer binding over base name;
|
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
|
| Sun, 16 Aug 2015 19:25:08 +0200 |
wenzelm |
added Thm.chyps_of;
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 15:43:45 +0200 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Sun, 31 May 2015 00:16:26 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 00:11:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 08 Mar 2015 20:34:53 +0100 |
wenzelm |
misc tuning and simplification;
|
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, 03 Mar 2015 19:08:04 +0100 |
traytel |
eliminated some clones of Proof_Context.cterm_of
|
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, 28 Jan 2015 14:24:29 +0100 |
eberlm |
Fixed bug in bugfix for function package
|
file |
diff |
annotate
|
| Wed, 28 Jan 2015 12:26:56 +0100 |
eberlm |
Fixed variable naming bug in function package
|
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, 07 Mar 2014 14:21:15 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Fri, 10 Jan 2014 21:37:28 +0100 |
wenzelm |
more elementary management of declared hyps, below structure Assumption;
|
file |
diff |
annotate
|
| Sat, 23 Nov 2013 17:07:36 +0100 |
wenzelm |
more accurate goal context;
|
file |
diff |
annotate
|
| Mon, 09 Sep 2013 00:14:07 +0200 |
krauss |
moved cases post-processing under mk_partial_rules_mutual, using existing bookkeeping information;
|
file |
diff |
annotate
|
| Sun, 08 Sep 2013 23:58:52 +0200 |
krauss |
clarified
|
file |
diff |
annotate
|
| Sun, 08 Sep 2013 23:49:25 +0200 |
krauss |
clarified, dropping unreachable bool special case
|
file |
diff |
annotate
|
| Sun, 08 Sep 2013 23:28:27 +0200 |
krauss |
dropped dead code
|
file |
diff |
annotate
|
| Sun, 08 Sep 2013 22:32:47 +0200 |
Manuel Eberl |
generate elim rules for elimination of function equalities;
|
file |
diff |
annotate
|
| Sun, 16 Jun 2013 22:56:44 +0200 |
krauss |
export dom predicate in the info record
|
file |
diff |
annotate
|