| Sat, 23 Jun 2007 19:33:22 +0200 |
nipkow |
tuned and renamed group_eq_simps and ring_eq_simps
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 19:49:14 +0200 |
huffman |
avoid using implicit prems in assumption
|
file |
diff |
annotate
|
| Wed, 20 Jun 2007 05:18:39 +0200 |
huffman |
change simp rules for of_nat to work like int did previously (reorient of_nat_Suc, remove of_nat_mult [simp]); preserve original variable names in legacy int theorems
|
file |
diff |
annotate
|
| Sun, 17 Jun 2007 18:47:03 +0200 |
nipkow |
tuned laws for cancellation in divisions for fields.
|
file |
diff |
annotate
|
| Sun, 17 Jun 2007 13:39:50 +0200 |
chaieb |
moved nonzero_mult_divide_cancel_right to Ring_and_Field as nonzero_mult_divide_cancel_right'; tuned proofs
|
file |
diff |
annotate
|
| Fri, 15 Jun 2007 15:10:32 +0200 |
nipkow |
made divide_self a simp rule
|
file |
diff |
annotate
|
| Tue, 05 Jun 2007 16:31:10 +0200 |
chaieb |
lemma lemma_DERIV_subst moved to Deriv.thy
|
file |
diff |
annotate
|
| Tue, 22 May 2007 07:29:49 +0200 |
huffman |
rename lemmas LIM_ident, isCont_ident, DERIV_ident
|
file |
diff |
annotate
|
| Sun, 20 May 2007 08:00:48 +0200 |
huffman |
change premises of DERIV_inverse_function lemma
|
file |
diff |
annotate
|
| Sun, 20 May 2007 03:19:14 +0200 |
huffman |
add lemma DERIV_inverse_function
|
file |
diff |
annotate
|
| Thu, 17 May 2007 21:51:32 +0200 |
huffman |
avoid using redundant lemmas from RealDef.thy
|
file |
diff |
annotate
|
| Wed, 16 May 2007 23:07:08 +0200 |
huffman |
section labels
|
file |
diff |
annotate
|
| Fri, 13 Apr 2007 00:07:52 +0200 |
huffman |
moved nonstandard derivative stuff from Deriv.thy into new file HDeriv.thy
|
file |
diff |
annotate
|
| Thu, 12 Apr 2007 03:37:30 +0200 |
huffman |
moved nonstandard limit stuff from Lim.thy into new theory HLim.thy
|
file |
diff |
annotate
|
| Sun, 08 Apr 2007 17:54:52 +0200 |
huffman |
remove redundant lemmas
|
file |
diff |
annotate
|