| Wed, 20 May 2020 19:43:39 +0000 |
haftmann |
generalized and augmented
|
file |
diff |
annotate
|
| Sun, 17 Nov 2019 20:44:35 +0000 |
haftmann |
strengthened type class for bit operations
|
file |
diff |
annotate
|
| Sun, 03 Nov 2019 16:20:05 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Thu, 08 Aug 2019 12:11:40 +0200 |
wenzelm |
prefer named lemmas -- more compact proofterms;
|
file |
diff |
annotate
|
| Sun, 06 Jan 2019 15:04:34 +0100 |
wenzelm |
isabelle update -u path_cartouches;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Mon, 26 Feb 2018 07:34:05 +0100 |
immler |
moved Lipschitz continuity from AFP/Ordinary_Differential_Equations and AFP/Gromov_Hyperbolicity; moved lemmas from AFP/Gromov_Hyperbolicity/Library_Complements
|
file |
diff |
annotate
|
| Wed, 10 Jan 2018 15:25:09 +0100 |
nipkow |
ran isabelle update_op on all sources
|
file |
diff |
annotate
|
| Wed, 07 Sep 2016 11:59:09 +0200 |
haftmann |
discontinued theory-local special syntax for lattice orderings
|
file |
diff |
annotate
|
| Wed, 10 Aug 2016 18:57:20 +0200 |
haftmann |
formal passive interpretation proofs for conj and disj
|
file |
diff |
annotate
|
| Tue, 02 Aug 2016 21:05:34 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Mon, 20 Jun 2016 17:03:50 +0200 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Sat, 11 Jun 2016 16:22:42 +0200 |
haftmann |
boldify syntax in abstract algebraic structures, to avoid clashes with concrete syntax in corresponding type classes
|
file |
diff |
annotate
|
| Mon, 07 Dec 2015 10:38:04 +0100 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Wed, 11 Nov 2015 09:21:56 +0100 |
Andreas Lochbihler |
cancel complementary terms as arguments to sup/inf in boolean algebras
|
file |
diff |
annotate
|
| Mon, 09 Nov 2015 15:48:17 +0100 |
wenzelm |
qualifier is mandatory by default;
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Tue, 01 Sep 2015 22:32:58 +0200 |
wenzelm |
eliminated \<Colon>;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Sun, 15 Feb 2015 17:01:22 +0100 |
haftmann |
explicit equivalence for strict order on lattices
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
explicit distributivity facts on min/max
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 15:52:25 +0100 |
haftmann |
postponed min/max lemmas until abstract lattice is available
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 15:52:25 +0100 |
haftmann |
prefer abstract simp rule
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 10:09:43 +0100 |
haftmann |
more lemmas on abstract lattices
|
file |
diff |
annotate
|
| Tue, 24 Dec 2013 11:24:16 +0100 |
haftmann |
tuning and augmentation of min/max lemmas;
|
file |
diff |
annotate
|
| Thu, 21 Nov 2013 21:33:34 +0100 |
blanchet |
rationalize imports
|
file |
diff |
annotate
|
| Thu, 25 Jul 2013 08:57:16 +0200 |
haftmann |
factored syntactic type classes for bot and top (by Alessandro Coglio)
|
file |
diff |
annotate
|
| Sun, 26 May 2013 19:45:54 +0200 |
haftmann |
examples for interpretation into target
|
file |
diff |
annotate
|
| Mon, 01 Apr 2013 17:42:29 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|