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 |