| Fri, 27 May 2016 20:23:55 +0200 |
wenzelm |
tuned proofs, to allow unfold_abs_def;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:47:08 +0200 |
wenzelm |
prefer tactics with explicit 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 20:47:29 +0100 |
wenzelm |
tuned;
|
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
|
| Fri, 19 Dec 2014 23:01:46 +0100 |
wenzelm |
just one data slot per program unit;
|
file |
diff |
annotate
|
| Wed, 29 Oct 2014 14:14:36 +0100 |
wenzelm |
modernized setup;
|
file |
diff |
annotate
|
| Sat, 16 Aug 2014 19:20:11 +0200 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| Fri, 21 Feb 2014 00:09:56 +0100 |
blanchet |
adapted to renaming of datatype 'cases' and 'recs' to 'case' and 'rec'
|
file |
diff |
annotate
|
| Sun, 12 Jan 2014 14:32:22 +0100 |
wenzelm |
tuned signature;
|
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
|
| Fri, 13 May 2011 23:58:40 +0200 |
wenzelm |
clarified map_simpset versus Simplifier.map_simpset_global;
|
file |
diff |
annotate
|
| Fri, 13 May 2011 22:55:00 +0200 |
wenzelm |
proper Proof.context for classical tactics;
|
file |
diff |
annotate
|
| Thu, 12 May 2011 22:46:21 +0200 |
wenzelm |
prefer plain simpset operations;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Mon, 10 Jan 2011 16:45:28 +0100 |
wenzelm |
added merge_options convenience;
|
file |
diff |
annotate
|
| Sun, 12 Dec 2010 21:41:01 +0100 |
krauss |
tuned headers
|
file |
diff |
annotate
|
| Wed, 03 Nov 2010 11:11:49 +0100 |
wenzelm |
replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 14:19:43 +0200 |
krauss |
removed complicated (and rarely helpful) error reporting
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 14:19:40 +0200 |
krauss |
discontinued continuations to simplify control flow; dropped optimization in scnp
|
file |
diff |
annotate
|
| Tue, 05 Oct 2010 14:19:38 +0200 |
krauss |
use Cache structure instead of passing tables around explicitly
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 17:01:12 +0200 |
wenzelm |
theory data merge: prefer left side uniformly;
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 11:52:04 +0200 |
krauss |
default termination prover as plain tactic
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 11:57:16 +0100 |
wenzelm |
modernized structure Local_Defs;
|
file |
diff |
annotate
|
| Sat, 02 Jan 2010 23:18:58 +0100 |
krauss |
absorb structures Decompose and Descent into Termination, to simplify further restructuring
|
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
|