| Sat, 25 Jun 2022 13:21:27 +0200 |
desharna |
moved mono and strict_mono to Fun and redefined them as abbreviations
|
file |
diff |
annotate
|
| Fri, 16 Jul 2021 14:43:25 +0100 |
paulson |
A few new lemmas and simplifications
|
file |
diff |
annotate
|
| Thu, 11 Mar 2021 07:05:38 +0000 |
haftmann |
avoid name clash
|
file |
diff |
annotate
|
| Fri, 10 Apr 2020 22:50:59 +0100 |
paulson |
more removal of applys
|
file |
diff |
annotate
|
| Sun, 09 Feb 2020 21:58:42 +0000 |
haftmann |
more rules for natural deduction from inequalities
|
file |
diff |
annotate
|
| Sat, 09 Nov 2019 10:38:51 +0000 |
haftmann |
new lemma
|
file |
diff |
annotate
|
| Wed, 09 Oct 2019 14:51:54 +0000 |
haftmann |
dedicated fact collections for algebraic simplification rules potentially splitting goals
|
file |
diff |
annotate
|
| Thu, 08 Aug 2019 12:11:40 +0200 |
wenzelm |
prefer named lemmas -- more compact proofterms;
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:28 +0000 |
haftmann |
official fact collection sign_simps
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Wed, 31 Oct 2018 15:53:32 +0100 |
wenzelm |
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
|
file |
diff |
annotate
|
| Tue, 18 Oct 2016 18:48:53 +0200 |
haftmann |
suitable logical type class for abs, sgn
|
file |
diff |
annotate
|
| Thu, 15 Sep 2016 10:40:10 +0200 |
hoelzl |
add add_eq_0_iff_both_eq_0 and zero_eq_add_iff_both_eq_0 to simp set
|
file |
diff |
annotate
|
| Fri, 12 Aug 2016 17:53:55 +0200 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 21:05:34 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2016 13:55:35 +0200 |
fleury |
sharing simp rules between ordered monoids and rings
|
file |
diff |
annotate
|
| Sat, 02 Jul 2016 08:41:05 +0200 |
haftmann |
abstract and concrete multiplicative groups
|
file |
diff |
annotate
|
| Mon, 20 Jun 2016 21:40:48 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Sat, 11 Jun 2016 16:22:42 +0200 |
haftmann |
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
|
file |
diff |
annotate
|
| Wed, 25 May 2016 11:49:40 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2016 10:22:46 +0100 |
haftmann |
more theorems on orderings
|
file |
diff |
annotate
|
| Mon, 22 Feb 2016 14:37:56 +0000 |
paulson |
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
|
file |
diff |
annotate
|
| Fri, 19 Feb 2016 13:40:50 +0100 |
hoelzl |
generalize more theorems to support enat and ennreal
|
file |
diff |
annotate
|
| Fri, 12 Feb 2016 16:09:07 +0100 |
hoelzl |
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
|
file |
diff |
annotate
|
| Wed, 10 Feb 2016 18:43:19 +0100 |
hoelzl |
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
generalized some lemmas;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 01:26:34 +0100 |
wenzelm |
prefer symbols for "abs";
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|