Tue, 09 Apr 2013 14:04:47 +0200 |
hoelzl |
move FrechetDeriv from the Library to HOL/Deriv; base DERIV on FDERIV and both derivatives allow a restricted support set; FDERIV is now an abbreviation of has_derivative
|
file |
diff |
annotate
|
Thu, 27 Sep 2012 14:52:50 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
Mon, 12 Sep 2011 07:55:43 +0200 |
nipkow |
new fastforce replacing fastsimp - less confusing name
|
file |
diff |
annotate
|
Thu, 18 Aug 2011 13:36:58 -0700 |
huffman |
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
|
file |
diff |
annotate
|
Wed, 10 Aug 2011 18:02:16 -0700 |
huffman |
avoid warnings about duplicate rules
|
file |
diff |
annotate
|
Thu, 09 Jun 2011 11:50:16 +0200 |
hoelzl |
lemma about differences of convex functions
|
file |
diff |
annotate
|
Mon, 23 Aug 2010 11:17:13 +0200 |
haftmann |
dropped type classes mult_mono and mult_mono1; tuned names of technical rule duplicates
|
file |
diff |
annotate
|
Sun, 09 May 2010 22:51:11 -0700 |
huffman |
avoid using real-specific versions of generic lemmas
|
file |
diff |
annotate
|
Tue, 04 May 2010 18:05:22 +0200 |
hoelzl |
Add Convex to Library build
|
file |
diff |
annotate
|
Mon, 03 May 2010 14:35:10 +0200 |
hoelzl |
Moved Convex theory to library.
|
file |
diff |
annotate
|