huffman [Thu, 17 May 2007 08:41:23 +0200] rev 22986
remove redundant instance declaration
huffman [Thu, 17 May 2007 00:45:27 +0200] rev 22985
cleaned up proof of Maclaurin_sin_bound
huffman [Wed, 16 May 2007 23:07:08 +0200] rev 22984
section labels
huffman [Wed, 16 May 2007 23:03:45 +0200] rev 22983
minimize imports
chaieb [Wed, 16 May 2007 09:45:22 +0200] rev 22982
dropped |R
chaieb [Tue, 15 May 2007 18:28:02 +0200] rev 22981
A verified theory for rational numbers representation and simple calculations;
verified with respect to the real numbers;
berghofe [Tue, 15 May 2007 18:20:07 +0200] rev 22980
Fixed bug that caused proof of induction theorem to fail if
introduction rules contained True or False.
huffman [Tue, 15 May 2007 08:10:31 +0200] rev 22979
minimize imports
huffman [Tue, 15 May 2007 07:28:08 +0200] rev 22978
clean up polar_Ex proofs; remove unnecessary lemmas
huffman [Tue, 15 May 2007 05:09:01 +0200] rev 22977
remove simp attribute from various polar_Ex lemmas
huffman [Mon, 14 May 2007 23:25:16 +0200] rev 22976
tuned proofs
huffman [Mon, 14 May 2007 23:09:54 +0200] rev 22975
spelling: rename arcos -> arccos
huffman [Mon, 14 May 2007 22:32:51 +0200] rev 22974
tuned proofs
huffman [Mon, 14 May 2007 20:48:32 +0200] rev 22973
add lemma sgn_mult; declare real_scaleR_def and scaleR_eq_0_iff as simp rules
huffman [Mon, 14 May 2007 20:14:31 +0200] rev 22972
generalized sgn function to work on any real normed vector space
huffman [Mon, 14 May 2007 19:14:50 +0200] rev 22971
root and sqrt on negative inputs
huffman [Mon, 14 May 2007 18:48:24 +0200] rev 22970
move lemmas to RealPow.thy; tuned proofs
huffman [Mon, 14 May 2007 18:04:52 +0200] rev 22969
tuned proofs
huffman [Mon, 14 May 2007 18:03:25 +0200] rev 22968
tuned
huffman [Mon, 14 May 2007 17:45:42 +0200] rev 22967
added general sum-squares lemmas
huffman [Mon, 14 May 2007 17:37:31 +0200] rev 22966
new lemmas
webertj [Mon, 14 May 2007 13:24:22 +0200] rev 22965
ProofGeneral: Find Theorems search form
haftmann [Mon, 14 May 2007 12:52:56 +0200] rev 22964
reorganized float arithmetic
haftmann [Mon, 14 May 2007 12:52:54 +0200] rev 22963
fixed IntInf ambiguity
huffman [Mon, 14 May 2007 09:33:18 +0200] rev 22962
remove redundant lemmas
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
wenzelm [Fri, 11 May 2007 01:07:10 +0200] rev 22933
tuned proofs;
wenzelm [Fri, 11 May 2007 00:43:46 +0200] rev 22932
bang_facts: warning;
wenzelm [Fri, 11 May 2007 00:43:45 +0200] rev 22931
tuned proofs;