chaieb [Mon, 11 Jun 2007 11:05:56 +0200] rev 23311
Context Data for the new presburger Method
chaieb [Mon, 11 Jun 2007 11:05:54 +0200] rev 23310
A new simpler and cleaner implementation of proof Synthesis for Presburger Arithmetic --- Cooper's Algorithm
huffman [Mon, 11 Jun 2007 07:10:06 +0200] rev 23309
remove references to constant int::nat=>int
huffman [Mon, 11 Jun 2007 06:14:32 +0200] rev 23308
simplify int proofs
huffman [Mon, 11 Jun 2007 05:20:05 +0200] rev 23307
modify proofs to avoid referring to int::nat=>int
huffman [Mon, 11 Jun 2007 02:25:55 +0200] rev 23306
add int_of_nat versions of lemmas about int::nat=>int
huffman [Mon, 11 Jun 2007 02:24:39 +0200] rev 23305
add lemma of_nat_power
huffman [Mon, 11 Jun 2007 01:22:29 +0200] rev 23304
add int_of_nat versions of lemmas about int::nat=>int
huffman [Mon, 11 Jun 2007 00:53:18 +0200] rev 23303
add abbreviation int_of_nat for of_nat::nat=>int;
add int_of_nat versions of all lemmas about int::nat=>int;
move int lemmas into their own section, preparing to remove
wenzelm [Sun, 10 Jun 2007 23:48:27 +0200] rev 23302
disabled theory "Reflected_Presburger" for smlnj (temporarily);