| Wed, 20 Mar 2024 11:11:04 +0100 |
desharna |
renamed lemma antisymp_on_reflcp to antisymp_on_reflclp
|
file |
diff |
annotate
|
| Wed, 20 Mar 2024 09:57:14 +0100 |
desharna |
tuned proof
|
file |
diff |
annotate
|
| Wed, 20 Mar 2024 09:26:25 +0100 |
desharna |
added lemma order_reflclp_if_transp_and_asymp
|
file |
diff |
annotate
|
| Wed, 20 Mar 2024 09:24:12 +0100 |
desharna |
added lemmas antisym_on_reflcl_if_asym_on and antisymp_on_reflclp_if_asymp_on
|
file |
diff |
annotate
|
| Thu, 29 Feb 2024 11:18:26 +0100 |
desharna |
added lemmas reflclp_(less|greater)_eq[simp], rtranclp_(less|greater)_eq[simp], and tranclp_(less|greater|less_eq|greater_eq)[simp]
|
file |
diff |
annotate
|
| Tue, 05 Mar 2024 15:02:31 +0100 |
desharna |
added lemmas rtranclp_ident_if_reflp_and_transp and tranclp_ident_if_transp
|
file |
diff |
annotate
|
| Mon, 19 Feb 2024 11:39:00 +0100 |
desharna |
added lemmas relpowp_left_unique and relpow_left_unique
|
file |
diff |
annotate
|
| Mon, 19 Feb 2024 11:21:06 +0100 |
desharna |
added lemmas relpowp_right_unique and relpow_right_unique
|
file |
diff |
annotate
|
| Wed, 14 Feb 2024 16:25:41 +0100 |
desharna |
added lemmas relpow_trans[trans] and relpowp_trans[trans]
|
file |
diff |
annotate
|
| Mon, 20 Mar 2023 15:01:12 +0100 |
desharna |
reversed import dependency between Relation and Finite_Set; and move theorems around
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 16:07:44 +0100 |
desharna |
strengthened and renamed trans_reflclI
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 16:05:57 +0100 |
desharna |
strengthened and renamed transp_reflclp
|
file |
diff |
annotate
|
| Fri, 16 Dec 2022 10:34:58 +0100 |
desharna |
strengthened and renamed symp_symclp
|
file |
diff |
annotate
|
| Thu, 15 Dec 2022 09:44:50 +0100 |
desharna |
added lemma antisymp_reflcp
|
file |
diff |
annotate
|
| Wed, 09 Nov 2022 15:38:43 +0100 |
desharna |
added lemma transp_reflclp[simp]
|
file |
diff |
annotate
|
| Wed, 09 Nov 2022 15:37:21 +0100 |
desharna |
added lemma reflclp_ident_if_reflp[simp]
|
file |
diff |
annotate
|
| Wed, 09 Nov 2022 16:39:45 +0100 |
desharna |
added lemma reflp_on_reflclp[simp]
|
file |
diff |
annotate
|
| Wed, 09 Nov 2022 16:45:12 +0100 |
desharna |
strengthened lemma reflp_rtranclp and renamed to reflp_on_rtranclp
|
file |
diff |
annotate
|
| 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
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Sun, 22 Jun 2014 12:37:55 +0200 |
nipkow |
r_into_(r)trancl should not be [simp]: helps little and comlicates some AFP proofs
|
file |
diff |
annotate
|
| Sat, 21 Jun 2014 15:46:52 +0200 |
nipkow |
added [simp]
|
file |
diff |
annotate
|
| Fri, 06 Jun 2014 10:53:33 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Sat, 22 Mar 2014 21:40:19 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Wed, 19 Feb 2014 08:34:33 +0100 |
blanchet |
moved 'primrec' up (for real this time) and removed temporary 'old_primrec'
|
file |
diff |
annotate
|
| Mon, 17 Feb 2014 13:31:42 +0100 |
blanchet |
renamed old 'primrec' to 'old_primrec' (until the new 'primrec' can be moved above 'Nat' in the theory dependencies)
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 08:37:06 +0100 |
blanchet |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
|
file |
diff |
annotate
|
| Tue, 12 Nov 2013 19:28:53 +0100 |
hoelzl |
add acyclicI_order
|
file |
diff |
annotate
|
| Thu, 18 Apr 2013 17:07:01 +0200 |
wenzelm |
simplifier uses proper Proof.context instead of historic type simpset;
|
file |
diff |
annotate
|
| Sun, 23 Dec 2012 19:54:15 +0100 |
nipkow |
renamed and added lemmas
|
file |
diff |
annotate
|
| Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|