| 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
|
| Wed, 17 Jul 2019 14:02:42 +0100 |
paulson |
a few new lemmas and a bit of tidying
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
slightly more specialized name for type class
|
file |
diff |
annotate
|
| Wed, 10 Apr 2019 21:29:32 +0100 |
paulson |
Fixing the main Homology theory; also moving a lot of sum/prod lemmas into their generic context
|
file |
diff |
annotate
|
| Wed, 10 Apr 2019 13:34:55 +0100 |
paulson |
The last big tranche of Homology material: invariance of domain; renamings to use generic sum/prod lemmas from their locale
|
file |
diff |
annotate
|
| Thu, 31 Jan 2019 13:08:59 +0000 |
haftmann |
proper congruence rule for image operator
|
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
|