| Thu, 19 Dec 2024 17:01:40 +0000 |
paulson |
revered the hiding of the standard nat theorems
|
file |
diff |
annotate
|
| Mon, 23 Sep 2024 13:32:38 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -u mixfix_cartouches -l Pure HOL" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Mon, 06 May 2024 14:39:33 +0100 |
paulson |
Some new simprules – and patches for proofs
|
file |
diff |
annotate
|
| Mon, 11 Mar 2024 15:07:02 +0000 |
paulson |
New material by Wenda Li and Manuel Eberl
|
file |
diff |
annotate
|
| Thu, 09 Nov 2023 15:11:51 +0000 |
haftmann |
explicit type class for discrete linordered semidoms
|
file |
diff |
annotate
|
| Thu, 02 Nov 2023 14:10:08 +0000 |
paulson |
fixed the simplification of Suc n - 1
|
file |
diff |
annotate
|
| Thu, 25 May 2023 13:58:46 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
| Tue, 23 May 2023 21:43:36 +0200 |
wenzelm |
more uniform simproc_setup: avoid vacuous abstraction over morphism, which sometimes captures context values in its functional closure;
|
file |
diff |
annotate
|
| Tue, 23 May 2023 12:31:23 +0100 |
paulson |
Finally, the abstract metric space development
|
file |
diff |
annotate
|
| Mon, 15 Aug 2022 12:50:24 +0100 |
paulson |
The same, without adding a new simprule
|
file |
diff |
annotate
|
| Sun, 14 Aug 2022 23:51:47 +0100 |
paulson |
moved some material from Sum_of_Powers
|
file |
diff |
annotate
|
| Fri, 22 Jul 2022 14:39:56 +0200 |
Fabian Huch |
tuned (some HOL lints, by Yecine Megdiche);
|
file |
diff |
annotate
|
| Sun, 11 Apr 2021 07:35:24 +0000 |
haftmann |
collected combinatorial material
|
file |
diff |
annotate
|
| Thu, 11 Mar 2021 07:05:38 +0000 |
haftmann |
avoid name clash
|
file |
diff |
annotate
|
| Thu, 21 May 2020 22:06:15 +0200 |
nipkow |
unused alias
|
file |
diff |
annotate
|
| Wed, 20 May 2020 19:43:39 +0000 |
haftmann |
generalized and augmented
|
file |
diff |
annotate
|
| Thu, 14 May 2020 23:44:01 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Mon, 04 May 2020 17:35:29 +0200 |
Manuel Eberl |
New HOL simproc 'datatype_no_proper_subterm'
|
file |
diff |
annotate
|
| Mon, 23 Mar 2020 10:25:56 +0000 |
paulson |
put back Nat.le_diff_conv2 because AUTO2 doesn't work with Groups.le_diff_conv2
|
file |
diff |
annotate
|
| Sun, 22 Mar 2020 17:21:16 +0000 |
paulson |
tidying up some horrible proofs
|
file |
diff |
annotate
|
| Sun, 09 Feb 2020 21:58:42 +0000 |
haftmann |
more rules for natural deduction from inequalities
|
file |
diff |
annotate
|
| Sun, 26 Jan 2020 20:35:31 +0000 |
haftmann |
generalized
|
file |
diff |
annotate
|
| Mon, 27 Jan 2020 14:32:43 +0000 |
paulson |
A few lemmas connected with orderings
|
file |
diff |
annotate
|
| Thu, 08 Aug 2019 12:11:40 +0200 |
wenzelm |
prefer named lemmas -- more compact proofterms;
|
file |
diff |
annotate
|
| Wed, 17 Jul 2019 14:02:42 +0100 |
paulson |
a few new lemmas and a bit of tidying
|
file |
diff |
annotate
|
| Sat, 22 Jun 2019 07:18:55 +0000 |
haftmann |
streamlined setup for linear algebra, particularly removed redundant rule declarations
|
file |
diff |
annotate
|
| Mon, 21 Jan 2019 14:44:23 +0000 |
paulson |
new material about summations and powers, along with some tweaks
|
file |
diff |
annotate
|
| Mon, 14 Jan 2019 18:35:03 +0000 |
haftmann |
tuned proofs
|
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
|