| Thu, 13 Mar 2025 09:48:39 +0100 |
desharna |
added lemmas irrefl_relation_ofD, refl_relation_ofD, total_relation_ofD
|
file |
diff |
annotate
|
| Thu, 13 Mar 2025 09:41:56 +0100 |
desharna |
added lemmas antisym_relation_of[simp], asym_relation_of[simp], sym_relation_of[simp], trans_relation_of[simp]
|
file |
diff |
annotate
|
| Tue, 11 Mar 2025 10:20:44 +0100 |
desharna |
changed definition of refl_on
|
file |
diff |
annotate
|
| Fri, 22 Jul 2022 14:39:56 +0200 |
Fabian Huch |
tuned (some HOL lints, by Yecine Megdiche);
|
file |
diff |
annotate
|
| Wed, 17 Apr 2019 21:48:56 +0200 |
nipkow |
added lemmas
|
file |
diff |
annotate
|
| Tue, 14 Aug 2018 16:05:40 +0100 |
paulson |
Zorn's lemma for relations defined by predicates
|
file |
diff |
annotate
|
| Fri, 22 Jun 2018 20:31:49 +0200 |
wenzelm |
clarified document antiquotation @{theory};
|
file |
diff |
annotate
|
| Wed, 28 Sep 2016 17:01:01 +0100 |
paulson |
new material connected with HOL Light measure theory, plus more rationalisation
|
file |
diff |
annotate
|
| Sun, 31 Jul 2016 22:56:18 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Fri, 29 Jul 2016 12:44:22 +0200 |
Andreas Lochbihler |
prefer [simp] over [iff] as [iff] break HOL-UNITY
|
file |
diff |
annotate
|
| Fri, 29 Jul 2016 09:49:23 +0200 |
Andreas Lochbihler |
add lemmas contributed by Peter Gammie
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Thu, 04 Sep 2014 14:02:37 +0200 |
hoelzl |
cleanup Wfrec; introduce dependent_wf/wellorder_choice
|
file |
diff |
annotate
|