2007-06-11 chaieb A new tactic for Presburger;
2007-06-11 chaieb tuned
2007-06-11 chaieb Temporarily added theorems for QE that were in old Presburger.thy ; This will diseappear with the new Ferrante and Rackoff shortly;
2007-06-11 chaieb tuned tactic
2007-06-11 chaieb Temporarily use int instead of IntInf.int but Code generator should map HOL's int to ML's IntInf.int --- To be fixed
2007-06-11 chaieb tuned Proof and Document
2007-06-11 chaieb tuned Proof
2007-06-11 chaieb A new and cleaned up Theory for QE. for Presburger arithmetic
2007-06-11 chaieb Added new files for Presburger (cooper_data.ML, cooper.ML) and deleted old unused ones cooper_dec, cooper_proof, reflected_cooper etc..
2007-06-11 chaieb explicitely depends on file groebner.ML
2007-06-11 chaieb Context Data for the new presburger Method
2007-06-11 chaieb A new simpler and cleaner implementation of proof Synthesis for Presburger Arithmetic --- Cooper's Algorithm
2007-06-11 huffman remove references to constant int::nat=>int
2007-06-11 huffman simplify int proofs
2007-06-11 huffman modify proofs to avoid referring to int::nat=>int
2007-06-11 huffman add int_of_nat versions of lemmas about int::nat=>int
2007-06-11 huffman add lemma of_nat_power
2007-06-10 huffman add int_of_nat versions of lemmas about int::nat=>int
2007-06-10 huffman add abbreviation int_of_nat for of_nat::nat=>int;
2007-06-10 wenzelm disabled theory "Reflected_Presburger" for smlnj (temporarily);
2007-06-10 wenzelm disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
2007-06-10 nipkow *** empty log message ***
2007-06-09 huffman remove dependencies of proofs on constant int::nat=>int, preparing to remove it
2007-06-08 wenzelm eqtype int -- explicitly encourage overloaded equality;
2007-06-08 wenzelm simplified type integer;
2007-06-08 berghofe Adapted Proofterm.bicompose_proof to Larry's changes in
2007-06-08 chaieb Method "algebra" solves polynomial equations over (semi)rings
2007-06-08 huffman generalize zpower_number_of_{even,odd} lemmas
(0) -10000 -3000 -1000 -300 -100 -50 -28 +28 +50 +100 +300 +1000 +3000 +10000 +30000 tip