| Fri, 22 Jul 2022 14:39:56 +0200 |
Fabian Huch |
tuned (some HOL lints, by Yecine Megdiche);
|
file |
diff |
annotate
|
| Tue, 05 Jul 2022 17:54:52 +0200 |
desharna |
added lemmas total_on_trancl and totalp_on_tranclp
|
file |
diff |
annotate
|
| Tue, 28 Sep 2021 17:09:05 +0200 |
wenzelm |
tuned antiquotations;
|
file |
diff |
annotate
|
| Tue, 21 Sep 2021 20:56:06 +0200 |
wenzelm |
clarified antiquotations;
|
file |
diff |
annotate
|
| Sun, 29 Mar 2020 21:30:52 +0100 |
paulson |
more ugly old proofs
|
file |
diff |
annotate
|
| Sun, 19 Jan 2020 07:50:35 +0100 |
traytel |
new examples of BNF lifting across quotients using a new theory of confluence,
|
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
|
| 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
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sat, 10 Nov 2018 07:57:20 +0000 |
haftmann |
replaced some ancient ASCII syntax
|
file |
diff |
annotate
|
| Thu, 12 Jul 2018 17:22:39 +0100 |
paulson |
de-applying (mostly Set_Interval)
|
file |
diff |
annotate
|
| Sat, 16 Jun 2018 22:09:24 +0200 |
nipkow |
more simp
|
file |
diff |
annotate
|
| Sat, 16 Jun 2018 20:32:00 +0200 |
nipkow |
moved lemmas from AFP
|
file |
diff |
annotate
|
| Sun, 25 Feb 2018 19:19:11 +0100 |
wenzelm |
more abbrevs;
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 12:11:00 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Fri, 05 Aug 2016 18:14:28 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Wed, 06 Jul 2016 20:19:51 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Tue, 12 Apr 2016 13:49:37 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 17 Feb 2016 21:51:56 +0100 |
haftmann |
prefer abbreviations for compound operators INFIMUM and SUPREMUM
|
file |
diff |
annotate
|
| Thu, 07 Jan 2016 15:53:39 +0100 |
wenzelm |
more uniform treatment of package internals;
|
file |
diff |
annotate
|
| Mon, 28 Dec 2015 21:47:32 +0100 |
wenzelm |
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sun, 15 Nov 2015 12:39:51 +0100 |
wenzelm |
option "inductive_defs" controls exposure of def and mono facts;
|
file |
diff |
annotate
|
| Tue, 13 Oct 2015 09:21:15 +0200 |
haftmann |
prod_case as canonical name for product type eliminator
|
file |
diff |
annotate
|
| Fri, 09 Oct 2015 20:26:03 +0200 |
wenzelm |
discontinued specific HTML syntax;
|
file |
diff |
annotate
|
| Thu, 27 Aug 2015 21:19:48 +0200 |
haftmann |
standardized some occurences of ancient "split" alias
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Tue, 07 Jul 2015 18:01:30 +0200 |
hoelzl |
add monotonicity rule for rtranclp
|
file |
diff |
annotate
|