| Sat, 06 Oct 2007 16:50:04 +0200 |
wenzelm |
simplified interfaces for outer syntax;
|
file |
diff |
annotate
|
| Fri, 05 Oct 2007 22:00:15 +0200 |
wenzelm |
tuned Induct interface: prefer pred'' over set'';
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 16:59:28 +0200 |
wenzelm |
Conv.forall_conv: proper context;
|
file |
diff |
annotate
|
| Thu, 04 Oct 2007 14:42:47 +0200 |
wenzelm |
moved Pure/Isar/induct_attrib.ML and Provers/induct_method.ML to Tools/induct.ML;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2007 10:35:53 +0200 |
berghofe |
prove_strong_ind now uses InductivePackage.rulify.
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 17:06:14 +0200 |
wenzelm |
proper Sign operations instead of Theory aliases;
|
file |
diff |
annotate
|
| 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
|