Wed, 18 Feb 2009 10:26:48 +0100 merged
blanchet [Wed, 18 Feb 2009 10:26:48 +0100] rev 29957
merged
Tue, 17 Feb 2009 14:01:54 +0100 Reintroduce set_interpreter for Collect and op :.
blanchet [Tue, 17 Feb 2009 14:01:54 +0100] rev 29956
Reintroduce set_interpreter for Collect and op :. I removed them by accident when removing old code that dealt with the "set" type. Incidentally, there is still some broken "set" code in Refute that should be fixed (see TODO in refute.ML).
Mon, 16 Feb 2009 20:33:23 +0100 Added Nitpick tag to 'of_int_of_nat'.
blanchet [Mon, 16 Feb 2009 20:33:23 +0100] rev 29955
Added Nitpick tag to 'of_int_of_nat'. This theorem leads to a more efficient encoding to Kodkod than the definition of 'of_int'.
Tue, 17 Feb 2009 20:45:23 -0800 add lemmas for exponentiation
huffman [Tue, 17 Feb 2009 20:45:23 -0800] rev 29954
add lemmas for exponentiation
Tue, 17 Feb 2009 21:51:52 +0100 merged
haftmann [Tue, 17 Feb 2009 21:51:52 +0100] rev 29953
merged
Tue, 17 Feb 2009 18:45:41 +0100 unified variable names in case expressions; no exponential fork in translation of case expressions
haftmann [Tue, 17 Feb 2009 18:45:41 +0100] rev 29952
unified variable names in case expressions; no exponential fork in translation of case expressions
Tue, 17 Feb 2009 10:52:55 -0800 merged
huffman [Tue, 17 Feb 2009 10:52:55 -0800] rev 29951
merged
Tue, 17 Feb 2009 07:13:29 -0800 remove redundant simp attributes for zdvd rules
huffman [Tue, 17 Feb 2009 07:13:29 -0800] rev 29950
remove redundant simp attributes for zdvd rules
Tue, 17 Feb 2009 06:59:33 -0800 lemmas abs_dvd_iff, dvd_abs_iff
huffman [Tue, 17 Feb 2009 06:59:33 -0800] rev 29949
lemmas abs_dvd_iff, dvd_abs_iff
Tue, 17 Feb 2009 18:48:17 +0100 Cleaned up IntDiv and removed subsumed lemmas.
nipkow [Tue, 17 Feb 2009 18:48:17 +0100] rev 29948
Cleaned up IntDiv and removed subsumed lemmas.
(0) -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip