Mon, 14 Jun 2010 15:10:36 +0200 | haftmann | removed simplifier congruence rule of "prod_case" | changeset | files |
Mon, 14 Jun 2010 10:36:01 +0200 | blanchet | adjusted the polymorphism handling of Skolem constants so that proof reconstruction doesn't fail in "equality_inf" | changeset | files |
Sat, 12 Jun 2010 15:48:17 +0200 | haftmann | merged | changeset | files |
Sat, 12 Jun 2010 15:47:50 +0200 | haftmann | declare lexn.simps [code del] | changeset | files |
Fri, 11 Jun 2010 17:14:02 +0200 | haftmann | declare lex_prod_def [code del] | changeset | files |
Fri, 11 Jun 2010 17:14:01 +0200 | haftmann | modernized specifications | changeset | files |
Fri, 11 Jun 2010 17:14:01 +0200 | haftmann | avoid references to old constdefs | changeset | files |