Fri, 19 Aug 2011 10:46:54 -0700Transcendental.thy: remove several unused lemmas and simplify some proofs
huffman [Fri, 19 Aug 2011 10:46:54 -0700] rev 45168
Transcendental.thy: remove several unused lemmas and simplify some proofs

Fri, 19 Aug 2011 08:40:15 -0700remove unused lemmas
huffman [Fri, 19 Aug 2011 08:40:15 -0700] rev 45167
remove unused lemmas

Fri, 19 Aug 2011 08:39:43 -0700fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas
huffman [Fri, 19 Aug 2011 08:39:43 -0700] rev 45166
fold definitions of sin_coeff and cos_coeff in Maclaurin lemmas

Fri, 19 Aug 2011 07:45:22 -0700remove some redundant simp rules
huffman [Fri, 19 Aug 2011 07:45:22 -0700] rev 45165
remove some redundant simp rules

Fri, 19 Aug 2011 17:05:10 +0900Quotient_Examples: Cset, List_Cset: Lift Inf and Sup directly.
Cezary Kaliszyk <kaliszyk@in.tum.de> [Fri, 19 Aug 2011 17:05:10 +0900] rev 45164
Quotient_Examples: Cset, List_Cset: Lift Inf and Sup directly.

Thu, 18 Aug 2011 22:32:19 -0700merged
huffman [Thu, 18 Aug 2011 22:32:19 -0700] rev 45163
merged

Thu, 18 Aug 2011 22:31:52 -0700define complex exponential 'expi' as abbreviation for 'exp'
huffman [Thu, 18 Aug 2011 22:31:52 -0700] rev 45162
define complex exponential 'expi' as abbreviation for 'exp'

Thu, 18 Aug 2011 21:23:31 -0700remove more bounded_linear locale interpretations (cf. f0de18b62d63)
huffman [Thu, 18 Aug 2011 21:23:31 -0700] rev 45161
remove more bounded_linear locale interpretations (cf. f0de18b62d63)

Thu, 18 Aug 2011 19:53:03 -0700optimize some proofs
huffman [Thu, 18 Aug 2011 19:53:03 -0700] rev 45160
optimize some proofs

Thu, 18 Aug 2011 18:10:23 -0700add Multivariate_Analysis dependencies
huffman [Thu, 18 Aug 2011 18:10:23 -0700] rev 45159
add Multivariate_Analysis dependencies