Fri, 13 Dec 2002 16:48:20 +0100 | paulson | integer induction rules | changeset | files |
Fri, 13 Dec 2002 14:20:47 +0100 | berghofe | size_of_proof no longer includes size_of_term | changeset | files |
Fri, 13 Dec 2002 13:47:13 +0100 | paulson | deleted redundant line | changeset | files |
Thu, 12 Dec 2002 11:38:18 +0100 | paulson | Better treatment of equality in premises of inductive definitions. Less | changeset | files |
Thu, 12 Dec 2002 11:33:48 +0100 | ballarin | Fixed error that affected document preperation. | changeset | files |
Wed, 11 Dec 2002 10:12:48 +0100 | ballarin | HOL/GroupTheory/Summation.thy added: summation operator for abelian groups. | changeset | files |
Tue, 10 Dec 2002 10:40:32 +0100 | berghofe | Added size_of_proof. | changeset | files |