| 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
|
| Fri, 19 Dec 2014 11:20:07 +0100 |
desharna |
use proper context in function
|
file |
diff |
annotate
|
| Sun, 09 Nov 2014 14:08:00 +0100 |
wenzelm |
proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
|
file |
diff |
annotate
|
| Mon, 18 Aug 2014 17:19:58 +0200 |
blanchet |
reordered some (co)datatype property names for more consistency
|
file |
diff |
annotate
|
| Fri, 27 Jun 2014 10:11:44 +0200 |
blanchet |
compile
|
file |
diff |
annotate
|
| Wed, 18 Jun 2014 17:42:24 +0200 |
blanchet |
made tactic more robust in the face of 'primcorec' specifications containing 'case_sum'
|
file |
diff |
annotate
|
| Fri, 07 Mar 2014 22:30:58 +0100 |
wenzelm |
more antiquotations;
|
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
|
| Thu, 06 Feb 2014 00:03:12 +0100 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Wed, 05 Feb 2014 23:30:02 +0100 |
blanchet |
adapted tactic to correctly handle 'if ... then ...' and 'case ...' under lambdas
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
tuned names
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
adjusted comments
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 18:24:56 +0100 |
blanchet |
avoid nested 'Tools' directories
|
file |
diff |
annotate
| base
|