| Thu, 13 Sep 2007 23:58:38 +0200 |
urbanc |
some cleaning up to do with contexts
|
file |
diff |
annotate
|
| Thu, 13 Sep 2007 18:11:59 +0200 |
berghofe |
Generalized equivariance and nominal_inductive commands to
|
file |
diff |
annotate
|
| Tue, 03 Jul 2007 17:17:06 +0200 |
wenzelm |
Conjunction.mk_conjunction_balanced;
|
file |
diff |
annotate
|
| Thu, 10 May 2007 00:39:46 +0200 |
wenzelm |
Thm.first_order_match;
|
file |
diff |
annotate
|
| Wed, 25 Apr 2007 15:22:57 +0200 |
berghofe |
eqvt_tac now instantiates introduction rules before applying them.
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 16:11:17 +0200 |
berghofe |
Modified eqvt_tac to avoid failure due to introduction rules
|
file |
diff |
annotate
|
| Thu, 19 Apr 2007 16:38:59 +0200 |
berghofe |
nominal_inductive no longer proves equivariance.
|
file |
diff |
annotate
|
| Wed, 28 Mar 2007 19:18:39 +0200 |
berghofe |
- Improved error messages in equivariance proof
|
file |
diff |
annotate
|
| Tue, 27 Mar 2007 17:55:09 +0200 |
berghofe |
Implemented proof of strong induction rule.
|
file |
diff |
annotate
|
| Tue, 13 Feb 2007 18:18:45 +0100 |
berghofe |
First steps towards strengthening of induction rules for
|
file |
diff |
annotate
|