| Mon, 11 Jun 2007 11:05:56 +0200 |
chaieb |
Context Data for the new presburger Method
|
changeset |
files
|
| Mon, 11 Jun 2007 11:05:54 +0200 |
chaieb |
A new simpler and cleaner implementation of proof Synthesis for Presburger Arithmetic --- Cooper's Algorithm
|
changeset |
files
|
| Mon, 11 Jun 2007 07:10:06 +0200 |
huffman |
remove references to constant int::nat=>int
|
changeset |
files
|
| Mon, 11 Jun 2007 06:14:32 +0200 |
huffman |
simplify int proofs
|
changeset |
files
|
| Mon, 11 Jun 2007 05:20:05 +0200 |
huffman |
modify proofs to avoid referring to int::nat=>int
|
changeset |
files
|
| Mon, 11 Jun 2007 02:25:55 +0200 |
huffman |
add int_of_nat versions of lemmas about int::nat=>int
|
changeset |
files
|
| Mon, 11 Jun 2007 02:24:39 +0200 |
huffman |
add lemma of_nat_power
|
changeset |
files
|
| Mon, 11 Jun 2007 01:22:29 +0200 |
huffman |
add int_of_nat versions of lemmas about int::nat=>int
|
changeset |
files
|
| Mon, 11 Jun 2007 00:53:18 +0200 |
huffman |
add abbreviation int_of_nat for of_nat::nat=>int;
|
changeset |
files
|
| Sun, 10 Jun 2007 23:48:27 +0200 |
wenzelm |
disabled theory "Reflected_Presburger" for smlnj (temporarily);
|
changeset |
files
|
| Sun, 10 Jun 2007 21:06:59 +0200 |
wenzelm |
disabled theories MIR and ReflectedFerrack for smlnj (temporarily);
|
changeset |
files
|
| Sun, 10 Jun 2007 10:23:42 +0200 |
nipkow |
*** empty log message ***
|
changeset |
files
|