huffman [Mon, 14 May 2007 09:27:24 +0200] rev 22961
remove redundant lemmas
huffman [Mon, 14 May 2007 09:16:47 +0200] rev 22960
remove redundant lemmas
huffman [Mon, 14 May 2007 09:11:30 +0200] rev 22959
remove redundant lemmas
huffman [Mon, 14 May 2007 08:15:13 +0200] rev 22958
cleaned up
huffman [Mon, 14 May 2007 08:12:38 +0200] rev 22957
tuned
huffman [Sun, 13 May 2007 20:05:42 +0200] rev 22956
define roots of negative reals so that many lemmas no longer require side conditions; simplification solves more goals than previously
huffman [Sun, 13 May 2007 19:15:36 +0200] rev 22955
add lemma power_eq_imp_eq_base
haftmann [Sun, 13 May 2007 18:16:49 +0200] rev 22954
added module int
haftmann [Sun, 13 May 2007 18:15:30 +0200] rev 22953
dropped legacy
haftmann [Sun, 13 May 2007 18:15:28 +0200] rev 22952
removed module rat.ML
haftmann [Sun, 13 May 2007 18:15:26 +0200] rev 22951
whitespace tuned
haftmann [Sun, 13 May 2007 18:15:25 +0200] rev 22950
tuned
haftmann [Sun, 13 May 2007 18:15:24 +0200] rev 22949
fixed omission
haftmann [Sun, 13 May 2007 18:15:23 +0200] rev 22948
tuned setup
haftmann [Sun, 13 May 2007 18:15:22 +0200] rev 22947
refined module rat
haftmann [Sun, 13 May 2007 18:15:21 +0200] rev 22946
added modules rat.ML and int.ML
nipkow [Sun, 13 May 2007 09:23:27 +0200] rev 22945
Removed junk
nipkow [Sun, 13 May 2007 07:11:21 +0200] rev 22944
Got rid of listsp
huffman [Sun, 13 May 2007 04:38:24 +0200] rev 22943
removed redundant lemmas
huffman [Sat, 12 May 2007 18:16:30 +0200] rev 22942
add lemma additive.setsum
nipkow [Fri, 11 May 2007 20:47:30 +0200] rev 22941
*** empty log message ***
nipkow [Fri, 11 May 2007 20:07:00 +0200] rev 22940
*** empty log message ***
wenzelm [Fri, 11 May 2007 18:49:15 +0200] rev 22939
proper type for fun/arg_cong_rule;
wenzelm [Fri, 11 May 2007 18:47:08 +0200] rev 22938
added fun/arg_cong_rule;
wenzelm [Fri, 11 May 2007 18:46:50 +0200] rev 22937
unified names: foo_conv;
wenzelm [Fri, 11 May 2007 17:54:36 +0200] rev 22936
tuned;
krauss [Fri, 11 May 2007 15:37:42 +0200] rev 22935
added fun flip f x y = f y x
huffman [Fri, 11 May 2007 03:31:12 +0200] rev 22934
generalize setsum lemmas from semiring_0_cancel to semiring_0