isabelle: File revisions

src/HOL/Library/Quotient_Set.thy

2013-08-13	kuncar	2013-08-13	*move Lifting/Transfer relevant parts of Library/Quotient_ to Main**	file \| diff \| annotate
2013-06-10	huffman	2013-06-10	more transfer rules for sets	file \| diff \| annotate
2013-05-15	kuncar	2013-05-15	stronger reflexivity prover	file \| diff \| annotate
2013-05-13	kuncar	2013-05-13	better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal	file \| diff \| annotate
2013-03-08	kuncar	2013-03-08	add [relator_mono] and [relator_distr] rules	file \| diff \| annotate
2012-05-24	kuncar	2012-05-24	prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule	file \| diff \| annotate
2012-05-16	kuncar	2012-05-16	infrastructure that makes possible to prove that a relation is reflexive	file \| diff \| annotate
2012-05-14	huffman	2012-05-14	add transfer rule for set_rel	file \| diff \| annotate
2012-04-26	kuncar	2012-04-26	use a quot_map theorem attribute instead of the complicated map attribute	file \| diff \| annotate
2012-04-22	huffman	2012-04-22	add transfer rule for set difference	file \| diff \| annotate
2012-04-22	huffman	2012-04-22	new example theory for quotient/transfer	file \| diff \| annotate
2012-04-21	huffman	2012-04-21	move alternative definition lemmas into Lifting.thy; simplify proof of Quotient_compose	file \| diff \| annotate
2012-04-21	huffman	2012-04-21	added covariant relator set_rel, with transfer rules for set operations	file \| diff \| annotate
2012-04-21	huffman	2012-04-21	renamed contravariant relator set_rel to vset_rel, to make room for new covariant relator	file \| diff \| annotate
2012-04-20	huffman	2012-04-20	move definition of set_rel into Library/Quotient_Set.thy	file \| diff \| annotate
2012-04-13	wenzelm	2012-04-13	updated headers;	file \| diff \| annotate
2012-04-03	kuncar	2012-04-03	new package Lifting - initial commit	file \| diff \| annotate
2012-03-23	kuncar	2012-03-23	store the relational theorem for every relator	file \| diff \| annotate
2011-12-24	haftmann	2011-12-24	adjusted to set/pred distinction by means of type constructor `set`	file \| diff \| annotate
2011-09-10	krauss	2011-09-10	mem_prs and mem_rsp in accordance with sets-as-predicates representation (backported from AFP/Coinductive)	file \| diff \| annotate
2011-08-24	Cezary Kaliszyk	2011-08-24	Quotient Package: add mem_rsp, mem_prs, tune proofs.	file \| diff \| annotate
2011-08-23	Cezary Kaliszyk	2011-08-23	Quotient Package: some infrastructure for lifting inside sets	file \| diff \| annotate

isabelle

RSS Atom