| Mon, 11 Jun 2007 11:06:13 +0200 | chaieb | Temporarily use int instead of IntInf.int but Code generator should map HOL's int to ML's IntInf.int --- To be fixed | changeset | files |
| Mon, 11 Jun 2007 11:06:11 +0200 | chaieb | tuned Proof and Document | changeset | files |
| Mon, 11 Jun 2007 11:06:04 +0200 | chaieb | tuned Proof | changeset | files |
| Mon, 11 Jun 2007 11:06:00 +0200 | chaieb | A new and cleaned up Theory for QE. for Presburger arithmetic | changeset | files |
| Mon, 11 Jun 2007 11:05:59 +0200 | chaieb | Added new files for Presburger (cooper_data.ML, cooper.ML) and deleted old unused ones cooper_dec, cooper_proof, reflected_cooper etc.. | changeset | files |
| Mon, 11 Jun 2007 11:05:57 +0200 | chaieb | explicitely depends on file groebner.ML | changeset | files |
| Mon, 11 Jun 2007 11:05:56 +0200 | chaieb | Context Data for the new presburger Method | changeset | files |