| Sun, 15 Nov 2020 07:17:06 +0000 |
haftmann |
bundles for reflected term syntax
|
file |
diff |
annotate
|
| Thu, 12 Nov 2020 09:06:44 +0100 |
haftmann |
bundled syntax for state monad combinators
|
file |
diff |
annotate
|
| Fri, 10 Apr 2020 22:50:59 +0100 |
paulson |
more removal of applys
|
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
|
| Fri, 14 Jun 2019 08:34:28 +0000 |
haftmann |
moved some theorems into HOL main corpus
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:28 +0000 |
haftmann |
official fact collection sign_simps
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
avoid pseudo-collection to be used in generated proofs
|
file |
diff |
annotate
|
| Fri, 14 Jun 2019 08:34:27 +0000 |
haftmann |
moved comment to approproiate place
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 29 Jun 2018 22:14:33 +0200 |
wenzelm |
merged;
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 21:05:56 +0200 |
wenzelm |
avoid pending shyps in global theory facts;
|
file |
diff |
annotate
|
| Thu, 28 Jun 2018 17:14:52 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Thu, 14 Jun 2018 10:51:12 +0200 |
nipkow |
removed duplicates
|
file |
diff |
annotate
|
| Sat, 11 Nov 2017 18:41:08 +0000 |
haftmann |
dedicated definition for coprimality
|
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
|
| Sat, 22 Apr 2017 22:01:35 +0200 |
wenzelm |
theories "GCD" and "Binomial" are already included in "Main": this avoids improper imports in applications;
|
file |
diff |
annotate
|
| Mon, 09 Jan 2017 18:53:20 +0100 |
haftmann |
moved some lemmas to appropriate places
|
file |
diff |
annotate
|
| Tue, 03 Jan 2017 16:48:49 +0000 |
paulson |
A few new lemmas and needed adaptations
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 17:33:07 +0200 |
nipkow |
setprod -> prod
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 11:46:22 +0200 |
nipkow |
setsum -> sum
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:04 +0200 |
haftmann |
more standardized names
|
file |
diff |
annotate
|
| Sun, 18 Sep 2016 16:59:15 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2016 10:23:49 +0200 |
boehmes |
more complete simpset for linear arithmetic to avoid warnings: terms such as (2x + 2y)/2 can then be simplified by the linear arithmetic prover during its proof replay
|
file |
diff |
annotate
|
| Fri, 15 Jul 2016 12:24:04 +0200 |
eberlm |
Merged
|
file |
diff |
annotate
|
| Thu, 14 Jul 2016 14:43:09 +0200 |
eberlm |
Tuned looping simp rules in semiring_div
|
file |
diff |
annotate
|
| Fri, 15 Jul 2016 11:07:51 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Mon, 20 Jun 2016 22:30:23 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 23 Feb 2016 16:25:08 +0100 |
nipkow |
more canonical names
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:57 +0100 |
haftmann |
dropped various legacy fact bindings
|
file |
diff |
annotate
|
| Wed, 06 Jan 2016 13:04:30 +0100 |
blanchet |
more complete setup for 'Rat' in Nitpick
|
file |
diff |
annotate
|