isabelle: File revisions

src/HOL/Lattices_Big.thy

2014-11-02	wenzelm	2014-11-02	modernized header uniformly as section;	file \| diff \| annotate
2014-09-28	haftmann	2014-09-28	moved to HOL and generalized	file \| diff \| annotate
2014-08-06	nipkow	2014-08-06	added lemma	file \| diff \| annotate
2014-05-19	hoelzl	2014-05-19	introduce Bochner integral: generalizes Lebesgue integral from real-valued function to functions on real-normed vector spaces	file \| diff \| annotate
2014-03-14	wenzelm	2014-03-14	just one cumulative Proof_Context.facts, with uniform retrieval (including PIDE markup, completion etc.); more thorough background_notes: distribute global notes to all contexts;	file \| diff \| annotate
2014-02-25	traytel	2014-02-25	joint work with blanchet: intermediate typedef for the input to fp-operations	file \| diff \| annotate
2014-01-20	blanchet	2014-01-20	swapped dependencies of 'Finite_Set' and 'Option' (to move BNF up)	file \| diff \| annotate
2013-12-27	haftmann	2013-12-27	prefer target-style syntaxx for sublocale	file \| diff \| annotate
2013-12-25	haftmann	2013-12-25	abolished slightly odd global lattice interpretation for min/max	file \| diff \| annotate
2013-12-25	haftmann	2013-12-25	prefer more canonical names for lemmas on min/max	file \| diff \| annotate
2013-12-24	haftmann	2013-12-24	tuning and augmentation of min/max lemmas; more lemmas and simp rules for abstract lattices with order; tuned proofs	file \| diff \| annotate
2013-12-15	haftmann	2013-12-15	disambiguation of interpretation prefixes	file \| diff \| annotate
2013-12-15	haftmann	2013-12-15	more algebraic terminology for theories about big operators	file \| diff \| annotate

isabelle

RSS Atom