| Wed, 09 Oct 2024 23:38:29 +0200 |
wenzelm |
more inner-syntax markup;
|
file |
diff |
annotate
|
| Mon, 29 Jan 2024 19:35:07 +0000 |
haftmann |
common type class for trivial properties on div/mod
|
file |
diff |
annotate
|
| Tue, 30 Apr 2019 17:03:32 +0100 |
paulson |
yet more de-applying
|
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
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 14:30:09 +0200 |
nipkow |
Prefix form of infix with * on either side no longer needs special treatment
|
file |
diff |
annotate
|
| Fri, 16 Feb 2018 21:40:15 +0100 |
wenzelm |
proper file name;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Sun, 08 Oct 2017 22:28:22 +0200 |
haftmann |
one uniform type class for parity structures
|
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, 18 Dec 2016 16:13:20 +0100 |
wenzelm |
more standard notation (like infix);
|
file |
diff |
annotate
|
| Tue, 01 Nov 2016 01:04:53 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 01 Nov 2016 00:44:24 +0100 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 18 Oct 2016 18:48:53 +0200 |
haftmann |
suitable logical type class for abs, sgn
|
file |
diff |
annotate
|
| Mon, 17 Oct 2016 15:23:06 +0200 |
Simon Wimmer |
Modified transfer principle in HOL/NSA to cause less ho-unficiation
|
file |
diff |
annotate
|
| Sun, 16 Oct 2016 09:31:05 +0200 |
haftmann |
more standardized theorem names for facts involving the div and mod identity
|
file |
diff |
annotate
|
| Mon, 26 Sep 2016 07:56:54 +0200 |
haftmann |
syntactic type class for operation mod named after mod;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2016 13:55:35 +0200 |
fleury |
sharing simp rules between ordered monoids and rings
|
file |
diff |
annotate
|
| Mon, 29 Feb 2016 22:34:36 +0100 |
wenzelm |
clarified session;
|
file |
diff |
annotate
| base
|