| Wed, 26 Aug 2009 19:54:01 +0200 | nipkow | got rid of complicated class finite_intvl_succ and defined "upto" directly on int, the only instance of the class. | changeset | files |
| Wed, 26 Aug 2009 17:38:18 +0100 | chaieb | merged | changeset | files |
| Wed, 26 Aug 2009 17:38:02 +0100 | chaieb | merged | changeset | files |
| Wed, 26 Aug 2009 17:34:32 +0100 | chaieb | removed unused theorem finite_Atleast_Atmost | changeset | files |
| Tue, 19 May 2009 14:13:37 +0100 | chaieb | merged | changeset | files |
| Tue, 19 May 2009 14:13:23 +0100 | chaieb | Derivative of general reverses | changeset | files |
| Wed, 26 Aug 2009 16:41:37 +0200 | nipkow | merged | changeset | files |
| Wed, 26 Aug 2009 16:13:19 +0200 | nipkow | new interval lemma | changeset | files |
| Wed, 26 Aug 2009 12:52:01 +0100 | paulson | merged | changeset | files |
| Wed, 26 Aug 2009 12:51:38 +0100 | paulson | Simplified some proofs using metis. | changeset | files |
| Fri, 21 Aug 2009 14:40:19 +0100 | paulson | merged | changeset | files |
| Fri, 14 Aug 2009 17:26:11 +0100 | paulson | sledgehammer used to streamline protocol proofs | changeset | files |