src/HOL/Lattices_Big.thy
Wed, 06 Aug 2014 18:03:43 +0200 nipkow added lemma
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
Fri, 14 Mar 2014 10:08:36 +0100 wenzelm just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.);
Tue, 25 Feb 2014 18:14:26 +0100 traytel joint work with blanchet: intermediate typedef for the input to fp-operations
Mon, 20 Jan 2014 23:34:26 +0100 blanchet swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)
Fri, 27 Dec 2013 14:35:14 +0100 haftmann prefer target-style syntaxx for sublocale
Wed, 25 Dec 2013 17:39:07 +0100 haftmann abolished slightly odd global lattice interpretation for min/max
Wed, 25 Dec 2013 17:39:06 +0100 haftmann prefer more canonical names for lemmas on min/max
Tue, 24 Dec 2013 11:24:16 +0100 haftmann tuning and augmentation of min/max lemmas;
Sun, 15 Dec 2013 15:10:16 +0100 haftmann disambiguation of interpretation prefixes
Sun, 15 Dec 2013 15:10:14 +0100 haftmann more algebraic terminology for theories about big operators
less more (0) tip