Thu, 14 Jun 2007 23:04:36 +0200 | wenzelm | tuned proofs: avoid implicit prems; | file | diff | annotate |
Fri, 27 Apr 2007 18:50:27 +0200 | urbanc | tuned some proofs in CR and properly included CR_Takahashi | 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:16:11 +0200 | berghofe | - Renamed <predicate>_eqvt to <predicate>.eqvt | file | diff | annotate |
Wed, 28 Mar 2007 17:27:44 +0200 | urbanc | adapted to new nominal_inductive | file | diff | annotate |
Mon, 27 Nov 2006 14:05:43 +0100 | urbanc | adapted function definitions to new syntax | file | diff | annotate |
Wed, 15 Nov 2006 16:23:55 +0100 | urbanc | replaced exists_fresh lemma with a version formulated with obtains; | file | diff | annotate |