| Thu, 14 Jun 2007 22:59:42 +0200 | chaieb | fixed term_constants (impact on is_relevant); terms in generalize_tac are sorted before we abstract over them (to *try* to avoid the case when a term to be abstracted over already occurs in an other) | changeset | files |
| Thu, 14 Jun 2007 22:59:40 +0200 | chaieb | no computation rules in the pre-simplifiaction set | changeset | files |
| Thu, 14 Jun 2007 22:59:39 +0200 | chaieb | Added some lemmas to default presburger simpset; tuned proofs | changeset | files |