| Tue, 04 Oct 2022 09:12:34 +0000 |
haftmann |
slightly less abusive proof pattern
|
file |
diff |
annotate
|
| Sat, 01 Oct 2022 07:56:53 +0000 |
haftmann |
reduce prominence of facts
|
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
|
| Tue, 13 Sep 2022 12:30:37 +0000 |
haftmann |
more concise instance-specific rules on euclidean relation
|
file |
diff |
annotate
|
| Mon, 05 Sep 2022 16:39:23 +0200 |
haftmann |
clarified generic euclidean relation
|
file |
diff |
annotate
|
| Wed, 31 Aug 2022 22:58:52 +0200 |
wenzelm |
eliminated tabs, assuming tab-width=4;
|
file |
diff |
annotate
|
| Sun, 21 Aug 2022 06:18:23 +0000 |
haftmann |
streamlined
|
file |
diff |
annotate
|
| Fri, 19 Aug 2022 05:49:12 +0000 |
haftmann |
streamlined theorems
|
file |
diff |
annotate
|
| Fri, 19 Aug 2022 05:49:11 +0000 |
haftmann |
more thorough split rules for div and mod on numerals, tuned split rules setup
|
file |
diff |
annotate
|
| Fri, 19 Aug 2022 05:49:07 +0000 |
haftmann |
streamlined theorems
|
file |
diff |
annotate
|
| Fri, 19 Aug 2022 05:49:06 +0000 |
haftmann |
streamlined theorems and sections
|
file |
diff |
annotate
|
| Wed, 17 Aug 2022 20:37:16 +0000 |
haftmann |
streamlined primitive definitions for integer division
|
file |
diff |
annotate
|
| Fri, 22 Jul 2022 14:39:56 +0200 |
Fabian Huch |
tuned (some HOL lints, by Yecine Megdiche);
|
file |
diff |
annotate
|
| Tue, 26 Oct 2021 14:43:59 +0000 |
haftmann |
more generic bit/word lemmas for distribution
|
file |
diff |
annotate
|
| Wed, 16 Jun 2021 08:19:09 +0000 |
haftmann |
more lemmas
|
file |
diff |
annotate
|
| Sun, 11 Apr 2021 07:35:24 +0000 |
haftmann |
collected combinatorial material
|
file |
diff |
annotate
|
| Tue, 06 Apr 2021 18:12:20 +0000 |
haftmann |
new lemmas
|
file |
diff |
annotate
|
| Fri, 21 Aug 2020 18:59:30 +0000 |
haftmann |
more lemmas
|
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
|
| Sat, 01 Feb 2020 19:10:40 +0100 |
haftmann |
more specific class assumptions
|
file |
diff |
annotate
|
| Sat, 01 Feb 2020 19:10:37 +0100 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| Sun, 26 Jan 2020 20:35:32 +0000 |
haftmann |
more theorems
|
file |
diff |
annotate
|
| Sat, 23 Nov 2019 09:56:11 +0000 |
haftmann |
tuned theory structure
|
file |
diff |
annotate
|
| Sat, 13 Apr 2019 08:43:33 +0000 |
haftmann |
backed out a93e6472ac9c, which does not bring anything substantial: division_ring is not commutative in multiplication but semidom_divide is
|
file |
diff |
annotate
|
| Tue, 09 Apr 2019 16:59:00 +0000 |
haftmann |
common type class for distributive division
|
file |
diff |
annotate
|
| Sat, 19 Jan 2019 20:40:17 +0000 |
haftmann |
algebraized more material from theory Divides
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 21:05:56 +0200 |
wenzelm |
avoid pending shyps in global theory facts;
|
file |
diff |
annotate
|
| Sat, 02 Dec 2017 16:50:53 +0000 |
haftmann |
more simplification rules
|
file |
diff |
annotate
|
| Thu, 23 Nov 2017 17:03:27 +0000 |
haftmann |
generalized more lemmas
|
file |
diff |
annotate
|
| Thu, 23 Nov 2017 13:00:00 +0000 |
haftmann |
new simp rule
|
file |
diff |
annotate
|
| Sat, 11 Nov 2017 18:41:08 +0000 |
haftmann |
dedicated definition for coprimality
|
file |
diff |
annotate
|
| Fri, 20 Oct 2017 07:46:10 +0200 |
haftmann |
added lemmas and tuned proofs
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:52 +0200 |
haftmann |
canonical multiplicative euclidean size
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:51 +0200 |
haftmann |
clarified parity
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:49 +0200 |
haftmann |
clarified uniqueness criterion for euclidean rings
|
file |
diff |
annotate
|
| Mon, 09 Oct 2017 19:10:48 +0200 |
haftmann |
tuned proofs
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
euclidean rings need no normalization
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
more fundamental definition of div and mod on int
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
generalized some rules
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
avoid variant of mk_sum
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
generalized simproc
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
elementary definition of division on natural numbers
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
tuned structure
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:21 +0200 |
haftmann |
abolished (semi)ring_div in favour of euclidean_(semi)ring_cancel
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:19 +0200 |
haftmann |
fundamental property of division by units
|
file |
diff |
annotate
|
| Wed, 04 Jan 2017 21:28:29 +0100 |
haftmann |
moved euclidean ring to HOL
|
file |
diff |
annotate
|