isabelle: File revisions

src/HOL/Probability/measurable.ML

2015-10-13	haftmann	2015-10-13	prod_case as canonical name for product type eliminator	file \| diff \| annotate
2015-07-27	wenzelm	2015-07-27	tuned;	file \| diff \| annotate
2015-07-27	wenzelm	2015-07-27	tuned signature;	file \| diff \| annotate
2015-04-09	wenzelm	2015-04-09	make SML/NJ more happy;	file \| diff \| annotate
2015-03-29	wenzelm	2015-03-29	tuned;	file \| diff \| annotate
2015-03-06	wenzelm	2015-03-06	Thm.cterm_of and Thm.ctyp_of operate on local context;	file \| diff \| annotate
2015-03-04	wenzelm	2015-03-04	tuned signature -- prefer qualified names;	file \| diff \| annotate
2015-02-10	wenzelm	2015-02-10	proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;	file \| diff \| annotate
2015-01-13	hoelzl	2015-01-13	measurability prover: removed app splitting, replaced by more powerful destruction rules	file \| diff \| annotate
2014-11-24	hoelzl	2014-11-24	add congruence solver to measurability prover	file \| diff \| annotate
2014-11-24	hoelzl	2014-11-24	cleanup measurability prover	file \| diff \| annotate
2014-11-11	Andreas Lochbihler	2014-11-11	add del option to measurable; make measurability rules available as dynamic theorem;	file \| diff \| annotate
2014-04-09	wenzelm	2014-04-09	proper context for print_tac;	file \| diff \| annotate
2013-12-31	wenzelm	2013-12-31	proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;	file \| diff \| annotate
2013-08-16	wenzelm	2013-08-16	more standard attribute_setup / method_setup -- export key ML operations instead of parsers;	file \| diff \| annotate
2013-04-18	wenzelm	2013-04-18	simplifier uses proper Proof.context instead of historic type simpset;	file \| diff \| annotate
2012-12-05	hoelzl	2012-12-05	Move the measurability prover to its own file	file \| diff \| annotate

isabelle

RSS Atom