paulson [Tue, 17 Feb 2009 10:03:58 +0000] rev 29895
Even and odd powers of -1
blanchet [Wed, 18 Feb 2009 10:26:48 +0100] rev 29894
merged
blanchet [Tue, 17 Feb 2009 14:01:54 +0100] rev 29893
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).
blanchet [Mon, 16 Feb 2009 20:33:23 +0100] rev 29892
Added Nitpick tag to 'of_int_of_nat'.
This theorem leads to a more efficient encoding to Kodkod than the definition of 'of_int'.
huffman [Tue, 17 Feb 2009 20:45:23 -0800] rev 29891
add lemmas for exponentiation
haftmann [Tue, 17 Feb 2009 21:51:52 +0100] rev 29890
merged
haftmann [Tue, 17 Feb 2009 18:45:41 +0100] rev 29889
unified variable names in case expressions; no exponential fork in translation of case expressions
huffman [Tue, 17 Feb 2009 10:52:55 -0800] rev 29888
merged
huffman [Tue, 17 Feb 2009 07:13:29 -0800] rev 29887
remove redundant simp attributes for zdvd rules
huffman [Tue, 17 Feb 2009 06:59:33 -0800] rev 29886
lemmas abs_dvd_iff, dvd_abs_iff