isabelle: Changelog

chaieb [Mon, 11 Jun 2007 11:07:18 +0200] rev 23324

Generated reflected QE procedure for Presburger Arithmetic-- Cooper's Algorithm -- see HOL/ex/Reflected_Presburger.thy

chaieb [Mon, 11 Jun 2007 11:06:23 +0200] rev 23323

Added more examples

chaieb [Mon, 11 Jun 2007 11:06:21 +0200] rev 23322

Now only contains generic conversion for quantifier elimination in HOL

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

isabelle