isabelle: File revisions

src/HOL/Library/FuncSet.thy

2013-09-03	wenzelm	2013-09-03	tuned proofs -- less guessing;	file \| diff \| annotate
2013-08-13	wenzelm	2013-08-13	standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;	file \| diff \| annotate
2012-11-19	hoelzl	2012-11-19	merge extensional dependent function space from FuncSet with the one in Finite_Product_Measure	file \| diff \| annotate
2012-11-16	hoelzl	2012-11-16	move theorems to be more generally useable	file \| diff \| annotate
2012-04-25	hoelzl	2012-04-25	moved lemmas to appropriate places	file \| diff \| annotate
2011-08-22	wenzelm	2011-08-22	reduced warnings;	file \| diff \| annotate
2010-11-22	bulwahn	2010-11-22	adding extensional function spaces to the FuncSet library theory	file \| diff \| annotate
2010-09-20	nipkow	2010-09-20	new lemmas	file \| diff \| annotate
2010-09-13	nipkow	2010-09-13	renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI	file \| diff \| annotate
2010-09-07	nipkow	2010-09-07	expand_fun_eq -> ext_iff expand_set_eq -> set_ext_iff Naming in line now with multisets	file \| diff \| annotate
2010-08-23	hoelzl	2010-08-23	Rewrite the Probability theory. Introduced pinfreal as real numbers with infinity. Use pinfreal as value for measures. Introduces Lebesgue Measure based on the integral in Multivariate Analysis. Proved Radon Nikodym for arbitrary sigma finite measure spaces.	file \| diff \| annotate
2009-10-28	paulson	2009-10-28	New theory Probability, which contains a development of measure theory	file \| diff \| annotate
2009-10-22	nipkow	2009-10-22	inv_onto -> inv_into	file \| diff \| annotate
2009-10-18	nipkow	2009-10-18	Inv -> inv_onto, inv abbr. inv_onto UNIV.	file \| diff \| annotate
2009-06-23	haftmann	2009-06-23	merged	file \| diff \| annotate
2009-06-23	haftmann	2009-06-23	lemma funcset_id by Jeremy Avigad	file \| diff \| annotate
2009-06-23	nipkow	2009-06-23	fixed name	file \| diff \| annotate
2009-06-22	nipkow	2009-06-22	tuned FuncSet	file \| diff \| annotate
2009-06-20	nipkow	2009-06-20	tuned	file \| diff \| annotate
2009-06-19	nipkow	2009-06-19	Made Pi_I [simp]	file \| diff \| annotate
2009-03-23	haftmann	2009-03-23	Main is (Complex_Main) base entry point in library theories	file \| diff \| annotate
2008-10-07	haftmann	2008-10-07	arbitrary is undefined	file \| diff \| annotate
2008-07-07	haftmann	2008-07-07	*absolute imports of HOL/.thy theories**	file \| diff \| annotate
2008-06-26	haftmann	2008-06-26	established Plain theory and image	file \| diff \| annotate
2008-06-12	wenzelm	2008-06-12	removed obsolete skolem declarations -- done by Theory.at_end;	file \| diff \| annotate
2008-02-21	nipkow	2008-02-21	moved bij_betw from Library/FuncSet to Fun, redistributed some lemmas	file \| diff \| annotate
2006-11-17	wenzelm	2006-11-17	more robust syntax for definition/abbreviation/notation;	file \| diff \| annotate
2006-11-07	wenzelm	2006-11-07	renamed 'const_syntax' to 'notation';	file \| diff \| annotate
2006-09-28	wenzelm	2006-09-28	fixed translations: CONST;	file \| diff \| annotate
2006-08-08	paulson	2006-08-08	skolem declarations for built-in theorems	file \| diff \| annotate
2006-05-27	wenzelm	2006-05-27	tuned;	file \| diff \| annotate
2006-05-16	wenzelm	2006-05-16	tuned concrete syntax -- abbreviation/const_syntax;	file \| diff \| annotate
2006-05-02	wenzelm	2006-05-02	replaced syntax/translations by abbreviation;	file \| diff \| annotate
2005-10-07	wenzelm	2005-10-07	print_translation: does not handle _idtdummy;	file \| diff \| annotate
2004-08-18	nipkow	2004-08-18	import -> imports	file \| diff \| annotate
2004-08-16	nipkow	2004-08-16	New theory header syntax.	file \| diff \| annotate
2004-06-01	paulson	2004-06-01	more on bij_betw	file \| diff \| annotate
2004-05-19	paulson	2004-05-19	new bij_betw operator	file \| diff \| annotate
2004-05-14	paulson	2004-05-14	new lemmas	file \| diff \| annotate
2004-05-06	wenzelm	2004-05-06	tuned document;	file \| diff \| annotate
2004-04-14	kleing	2004-04-14	use more symbols in HTML output	file \| diff \| annotate
2002-09-27	paulson	2002-09-27	Proof tidying	file \| diff \| annotate
2002-09-27	paulson	2002-09-27	Tidied. New Pi-theorem.	file \| diff \| annotate
2002-09-26	paulson	2002-09-26	new theory for Pi-sets, restrict, etc.	file \| diff \| annotate

isabelle

RSS Atom