huffman [Wed, 18 Feb 2009 12:24:06 -0800] rev 29979
add some lemmas, cleaned up
huffman [Wed, 18 Feb 2009 10:24:48 -0800] rev 29978
generalize le_imp_power_dvd and power_le_dvd; move from Divides to Power
huffman [Wed, 18 Feb 2009 09:47:58 -0800] rev 29977
move polynomial order stuff from Fundamental_Theorem_Algebra to Polynomial
huffman [Wed, 18 Feb 2009 09:08:04 -0800] rev 29976
merged
huffman [Wed, 18 Feb 2009 09:07:36 -0800] rev 29975
more subsection headings
huffman [Wed, 18 Feb 2009 07:24:13 -0800] rev 29974
speed up proof of exp_exists
haftmann [Wed, 18 Feb 2009 19:18:34 +0100] rev 29973
tuned
haftmann [Wed, 18 Feb 2009 19:18:33 +0100] rev 29972
sort instances wrt. to class hierarchy
haftmann [Wed, 18 Feb 2009 19:18:33 +0100] rev 29971
fixed signature
haftmann [Wed, 18 Feb 2009 19:18:32 +0100] rev 29970
tuned accessor name
haftmann [Wed, 18 Feb 2009 19:18:32 +0100] rev 29969
more precise improvement in instantiation user space type system
haftmann [Wed, 18 Feb 2009 19:18:31 +0100] rev 29968
do not drop arguments to 0, 1
haftmann [Wed, 18 Feb 2009 13:39:16 +0100] rev 29967
merged
haftmann [Wed, 18 Feb 2009 13:39:05 +0100] rev 29966
reverted to previous version of Finite_Set.thy
haftmann [Wed, 18 Feb 2009 11:31:05 +0100] rev 29965
merged
haftmann [Wed, 18 Feb 2009 08:23:45 +0100] rev 29964
merged
haftmann [Wed, 18 Feb 2009 08:23:12 +0100] rev 29963
first working version
haftmann [Wed, 18 Feb 2009 08:23:11 +0100] rev 29962
tuned comments, stripped ID, deleted superfluous code
haftmann [Wed, 18 Feb 2009 08:23:11 +0100] rev 29961
stripped ID
paulson [Wed, 18 Feb 2009 11:18:01 +0000] rev 29960
Syntactic support for products over set intervals
paulson [Wed, 18 Feb 2009 11:17:29 +0000] rev 29959
No idea what happened here!
paulson [Tue, 17 Feb 2009 10:03:58 +0000] rev 29958
Even and odd powers of -1
blanchet [Wed, 18 Feb 2009 10:26:48 +0100] rev 29957
merged
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).
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'.
huffman [Tue, 17 Feb 2009 20:45:23 -0800] rev 29954
add lemmas for exponentiation
haftmann [Tue, 17 Feb 2009 21:51:52 +0100] rev 29953
merged
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
huffman [Tue, 17 Feb 2009 10:52:55 -0800] rev 29951
merged
huffman [Tue, 17 Feb 2009 07:13:29 -0800] rev 29950
remove redundant simp attributes for zdvd rules