| Wed, 02 Dec 2015 19:14:57 +0100 |
haftmann |
modernized
|
file |
diff |
annotate
|
| Mon, 09 Nov 2015 15:48:17 +0100 |
wenzelm |
qualifier is mandatory by default;
|
file |
diff |
annotate
|
| Wed, 04 Nov 2015 08:13:52 +0100 |
ballarin |
Keyword 'rewrites' identifies rewrite morphisms.
|
file |
diff |
annotate
|
| Sun, 13 Sep 2015 22:56:52 +0200 |
wenzelm |
tuned proofs -- less legacy;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 22:58:50 +0200 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| Thu, 13 Nov 2014 17:19:52 +0100 |
hoelzl |
import general theorems from AFP/Markov_Models
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Sun, 28 Sep 2014 20:27:46 +0200 |
haftmann |
moved to HOL and generalized
|
file |
diff |
annotate
|
| Wed, 06 Aug 2014 18:03:43 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Mon, 19 May 2014 12:04:45 +0200 |
hoelzl |
introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces
|
file |
diff |
annotate
|
| Fri, 14 Mar 2014 10:08:36 +0100 |
wenzelm |
just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 18:14:26 +0100 |
traytel |
joint work with blanchet: intermediate typedef for the input to fp-operations
|
file |
diff |
annotate
|
| Mon, 20 Jan 2014 23:34:26 +0100 |
blanchet |
swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
|
file |
diff |
annotate
|
| Fri, 27 Dec 2013 14:35:14 +0100 |
haftmann |
prefer target-style syntaxx for sublocale
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:07 +0100 |
haftmann |
abolished slightly odd global lattice interpretation for min/max
|
file |
diff |
annotate
|
| Wed, 25 Dec 2013 17:39:06 +0100 |
haftmann |
prefer more canonical names for lemmas on min/max
|
file |
diff |
annotate
|
| Tue, 24 Dec 2013 11:24:16 +0100 |
haftmann |
tuning and augmentation of min/max lemmas;
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 15:10:16 +0100 |
haftmann |
disambiguation of interpretation prefixes
|
file |
diff |
annotate
|
| Sun, 15 Dec 2013 15:10:14 +0100 |
haftmann |
more algebraic terminology for theories about big operators
|
file |
diff |
annotate
|