Mon, 11 Jun 2007 11:06:21 +0200 Now only contains generic conversion for quantifier elimination in HOL
chaieb [Mon, 11 Jun 2007 11:06:21 +0200] rev 23322
Now only contains generic conversion for quantifier elimination in HOL
Mon, 11 Jun 2007 11:06:19 +0200 A new tactic for Presburger;
chaieb [Mon, 11 Jun 2007 11:06:19 +0200] rev 23321
A new tactic for Presburger;
Mon, 11 Jun 2007 11:06:18 +0200 tuned
chaieb [Mon, 11 Jun 2007 11:06:18 +0200] rev 23320
tuned
Mon, 11 Jun 2007 11:06:17 +0200 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: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;
Mon, 11 Jun 2007 11:06:15 +0200 tuned tactic
chaieb [Mon, 11 Jun 2007 11:06:15 +0200] rev 23318
tuned tactic
Mon, 11 Jun 2007 11:06:13 +0200 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: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
Mon, 11 Jun 2007 11:06:11 +0200 tuned Proof and Document
chaieb [Mon, 11 Jun 2007 11:06:11 +0200] rev 23316
tuned Proof and Document
Mon, 11 Jun 2007 11:06:04 +0200 tuned Proof
chaieb [Mon, 11 Jun 2007 11:06:04 +0200] rev 23315
tuned Proof
Mon, 11 Jun 2007 11:06:00 +0200 A new and cleaned up Theory for QE. for Presburger arithmetic
chaieb [Mon, 11 Jun 2007 11:06:00 +0200] rev 23314
A new and cleaned up Theory for QE. for Presburger arithmetic
Mon, 11 Jun 2007 11:05:59 +0200 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: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..
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip