chaieb [Mon, 11 Jun 2007 11:06:19 +0200] rev 23321
A new tactic for Presburger;
chaieb [Mon, 11 Jun 2007 11:06:18 +0200] rev 23320
tuned
chaieb [Mon, 11 Jun 2007 11:06:17 +0200] rev 23319
Temporarily added theorems for QE that were in old Presburger.thy ; This will diseappear with the new Ferrante and Rackoff shortly;
chaieb [Mon, 11 Jun 2007 11:06:15 +0200] rev 23318
tuned tactic
chaieb [Mon, 11 Jun 2007 11:06:13 +0200] rev 23317
Temporarily use int instead of IntInf.int but Code generator should map HOL's int to ML's IntInf.int --- To be fixed
chaieb [Mon, 11 Jun 2007 11:06:11 +0200] rev 23316
tuned Proof and Document
chaieb [Mon, 11 Jun 2007 11:06:04 +0200] rev 23315
tuned Proof
chaieb [Mon, 11 Jun 2007 11:06:00 +0200] rev 23314
A new and cleaned up Theory for QE. for Presburger arithmetic
chaieb [Mon, 11 Jun 2007 11:05:59 +0200] rev 23313
Added new files for Presburger (cooper_data.ML, cooper.ML) and deleted old unused ones cooper_dec, cooper_proof, reflected_cooper etc..
chaieb [Mon, 11 Jun 2007 11:05:57 +0200] rev 23312
explicitely depends on file groebner.ML