| Wed, 05 Jul 2023 16:50:07 +0100 |
paulson |
A couple of new lemmas involving cardinality
|
file |
diff |
annotate
|
| Tue, 02 May 2023 15:17:39 +0100 |
paulson |
More new theorems, and a necessary correction
|
file |
diff |
annotate
|
| Thu, 29 Sep 2022 14:03:40 +0000 |
haftmann |
moved relevant theorems from theory Divides to theory Euclidean_Division
|
file |
diff |
annotate
|
| Fri, 22 Jul 2022 14:39:56 +0200 |
Fabian Huch |
tuned (some HOL lints, by Yecine Megdiche);
|
file |
diff |
annotate
|
| Fri, 15 Jul 2022 09:18:21 +0200 |
nipkow |
moved lemma fromm AFP
|
file |
diff |
annotate
|
| Wed, 08 Jun 2022 15:36:27 +0100 |
paulson |
some additional lemmas and a little tidying up
|
file |
diff |
annotate
|
| Tue, 17 May 2022 14:10:14 +0100 |
paulson |
tidied auto / simp with null arguments
|
file |
diff |
annotate
|
| Fri, 18 Feb 2022 21:40:01 +0000 |
paulson |
one new lemma
|
file |
diff |
annotate
|
| Wed, 05 Jan 2022 15:35:23 +0000 |
paulson |
New and simplified theorems
|
file |
diff |
annotate
|
| Sun, 26 Dec 2021 11:01:27 +0000 |
paulson |
Tiny additions inspired by Roth development
|
file |
diff |
annotate
|
| Mon, 06 Dec 2021 12:39:59 +0100 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Mon, 02 Aug 2021 10:01:06 +0000 |
haftmann |
moved theory Bit_Operations into Main corpus
|
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
|
| Wed, 20 Jan 2021 09:46:01 +0100 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Sun, 22 Nov 2020 18:26:45 +0000 |
paulson |
cleanup of old proofs
|
file |
diff |
annotate
|
| Fri, 25 Sep 2020 14:11:48 +0100 |
paulson |
fixed some remarkably ugly proofs
|
file |
diff |
annotate
|
| Fri, 18 Sep 2020 08:02:19 +0100 |
paulson |
removal of needless premises
|
file |
diff |
annotate
|
| Fri, 08 May 2020 06:26:28 +0000 |
haftmann |
prefer _ mod 2 over of_bool (odd _)
|
file |
diff |
annotate
|
| Mon, 06 Apr 2020 19:46:38 +0100 |
paulson |
a few more applys
|
file |
diff |
annotate
|
| Sun, 08 Mar 2020 17:07:49 +0000 |
haftmann |
more frugal simp rules for bit operations; more pervasive use of bit selector
|
file |
diff |
annotate
|
| Wed, 26 Feb 2020 12:21:48 +0000 |
paulson |
Moved a number of general-purpose lemmas into HOL
|
file |
diff |
annotate
|
| Sun, 16 Feb 2020 18:01:03 +0100 |
nipkow |
lemmas about "card A = 2"; prefer iff to implications
|
file |
diff |
annotate
|
| Mon, 09 Dec 2019 15:36:51 +0000 |
paulson |
a few new and tidier proofs (mostly about finite sets)
|
file |
diff |
annotate
|
| Tue, 26 Nov 2019 14:32:08 +0000 |
paulson |
Rearrangement of material in Complex_Analysis_Basics, which contained much that had nothing to do with complex analysis.
|
file |
diff |
annotate
|
| Sat, 09 Nov 2019 15:39:21 +0000 |
haftmann |
bit shifts as class operations
|
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
|
| Tue, 24 Sep 2019 12:56:10 +0100 |
paulson |
More type class generalisations. Note that linorder_antisym_conv1 and linorder_antisym_conv2 no longer exist.
|
file |
diff |
annotate
|
| Mon, 23 Sep 2019 14:08:49 +0100 |
paulson |
Generalisation of many theorems to a more abstract type class (suggested by Mr Anonymous)
|
file |
diff |
annotate
|
| Wed, 18 Sep 2019 14:41:37 +0100 |
paulson |
imported new material mostly due to Sébastien Gouëzel
|
file |
diff |
annotate
|