| Sat, 05 Jul 2014 11:01:53 +0200 |
haftmann |
prefer ac_simps collections over separate name bindings for add and mult
|
file |
diff |
annotate
|
| Fri, 04 Jul 2014 20:18:47 +0200 |
haftmann |
reduced name variants for assoc and commute on plus and mult
|
file |
diff |
annotate
|
| Sat, 28 Jun 2014 09:16:42 +0200 |
haftmann |
fact consolidation
|
file |
diff |
annotate
|
| Fri, 11 Apr 2014 13:36:57 +0200 |
nipkow |
made mult_nonneg_nonneg a simp rule
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 09:37:48 +0200 |
hoelzl |
field_simps: better support for negation and division, and power
|
file |
diff |
annotate
|
| Wed, 09 Apr 2014 09:37:47 +0200 |
hoelzl |
revert c1bbd3e22226, a14831ac3023, and 36489d77c484: divide_minus_left/right are again simp rules
|
file |
diff |
annotate
|
| Sun, 06 Apr 2014 19:35:35 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 03 Apr 2014 23:51:52 +0100 |
paulson |
removing simprule status for divide_minus_left and divide_minus_right
|
file |
diff |
annotate
|
| Tue, 18 Mar 2014 09:39:07 -0700 |
huffman |
remove unnecessary finiteness assumptions from lemmas about setsum
|
file |
diff |
annotate
|
| Sun, 16 Mar 2014 18:09:04 +0100 |
haftmann |
normalising simp rules for compound operators
|
file |
diff |
annotate
|
| Tue, 04 Mar 2014 14:14:28 -0800 |
huffman |
tuned proof
|
file |
diff |
annotate
|
| Thu, 27 Feb 2014 16:07:21 +0000 |
paulson |
A bit of tidying up
|
file |
diff |
annotate
|
| Sat, 25 Jan 2014 16:45:13 +0100 |
wenzelm |
tuned proof;
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
summarized notions related to ordered_euclidean_space and intervals in separate theory
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
introduced ordered real vector spaces
|
file |
diff |
annotate
|
| Mon, 16 Dec 2013 17:08:22 +0100 |
immler |
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
|
file |
diff |
annotate
|
| Mon, 09 Dec 2013 12:22:23 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Tue, 19 Nov 2013 10:05:53 +0100 |
haftmann |
eliminiated neg_numeral in favour of - (numeral _)
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 19:28:54 +0100 |
hoelzl |
add finite_select_induct; move generic lemmas from MV_Analysis/Linear_Algebra to the HOL image
|
file |
diff |
annotate
|
| Fri, 01 Nov 2013 18:51:14 +0100 |
haftmann |
more simplification rules on unary and binary minus
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 16:33:34 -0700 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| Thu, 26 Sep 2013 16:33:32 -0700 |
huffman |
moved lemma
|
file |
diff |
annotate
|
| Tue, 24 Sep 2013 16:03:00 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 18 Sep 2013 20:32:11 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 18:09:17 -0700 |
huffman |
make 'linear' into a sublocale of 'bounded_linear';
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 09:33:36 -0700 |
huffman |
new lemmas
|
file |
diff |
annotate
|
| Thu, 12 Sep 2013 09:06:46 -0700 |
huffman |
prefer theorem name over 'long_thm_list(n)'
|
file |
diff |
annotate
|
| Wed, 04 Sep 2013 17:36:37 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Sun, 18 Aug 2013 19:59:19 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|