isabelle: File revisions

src/HOL/Relation.thy

2012-03-12	noschinl	2012-03-12	tuned simpset	file \| diff \| annotate
2012-03-07	haftmann	2012-03-07	tuned syntax; more candidates	file \| diff \| annotate
2012-03-02	haftmann	2012-03-02	more fundamental pred-to-set conversions for range and domain by means of inductive_set	file \| diff \| annotate
2012-03-01	haftmann	2012-03-01	more fundamental pred-to-set conversions, particularly by means of inductive_set; associated consolidation of some theorem names (c.f. NEWS)	file \| diff \| annotate
2012-02-26	haftmann	2012-02-26	restored accidental omission	file \| diff \| annotate
2012-02-26	haftmann	2012-02-26	tuned structure	file \| diff \| annotate
2012-02-26	haftmann	2012-02-26	tuned structure; dropped already existing syntax declarations	file \| diff \| annotate
2012-02-26	haftmann	2012-02-26	tuned syntax declarations; tuned structure	file \| diff \| annotate
2012-02-26	haftmann	2012-02-26	marked candidates for rule declarations	file \| diff \| annotate
2012-02-24	haftmann	2012-02-24	moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy	file \| diff \| annotate
2012-02-24	haftmann	2012-02-24	given up disfruitful branch	file \| diff \| annotate
2012-02-24	haftmann	2012-02-24	explicit remove of lattice notation	file \| diff \| annotate
2012-02-23	haftmann	2012-02-23	moved predicate relations and conversion rules between set and predicate relations from Predicate.thy to Relation.thy; moved Predicate.thy upwards in theory hierarchy	file \| diff \| annotate
2012-01-30	nipkow	2012-01-30	added "'a rel"	file \| diff \| annotate
2012-01-01	haftmann	2012-01-01	cleanup of code declarations	file \| diff \| annotate
2011-12-24	haftmann	2011-12-24	dropped obsolete code equation for Id	file \| diff \| annotate
2011-10-13	haftmann	2011-10-13	moved acyclic predicate up in hierarchy	file \| diff \| annotate
2011-10-13	haftmann	2011-10-13	modernized definitions	file \| diff \| annotate
2011-09-20	haftmann	2011-09-20	tuned specification and lemma distribution among theories; tuned proofs	file \| diff \| annotate
2011-09-13	huffman	2011-09-13	tuned proofs	file \| diff \| annotate
2011-08-18	haftmann	2011-08-18	observe distinction between sets and predicates more properly	file \| diff \| annotate
2011-02-21	blanchet	2011-02-21	renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics	file \| diff \| annotate
2010-12-07	bulwahn	2010-12-07	adding a definition for refl_on which is friendly for quickcheck and nitpick	file \| diff \| annotate
2010-12-03	bulwahn	2010-12-03	adding a nice definition of Id_on for quickcheck and nitpick	file \| diff \| annotate
2010-05-09	krauss	2010-05-09	added lemmas rel_comp_UNION_distrib(2)	file \| diff \| annotate
2010-05-07	krauss	2010-05-07	removed semicolons	file \| diff \| annotate
2010-05-07	krauss	2010-05-07	rule subrelI (for nice Isar proofs of relation inequalities)	file \| diff \| annotate
2010-03-18	blanchet	2010-03-18	now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"	file \| diff \| annotate
2009-10-26	krauss	2009-10-26	lemma converse_inv_image	file \| diff \| annotate
2009-10-05	paulson	2009-10-05	New facts about domain and range in	file \| diff \| annotate
2009-10-01	haftmann	2009-10-01	proper merge of interpretation equations	file \| diff \| annotate
2009-08-31	krauss	2009-08-31	moved lemma Wellfounded.in_inv_image to Relation.thy	file \| diff \| annotate
2009-07-27	krauss	2009-07-27	"more standard" argument order of relation composition (op O)	file \| diff \| annotate
2009-04-28	haftmann	2009-04-28	ephermal enforcement of import order to circumvent current problem in merging interpretation morphisms	file \| diff \| annotate
2009-03-02	nipkow	2009-03-02	name changes	file \| diff \| annotate
2009-02-11	nipkow	2009-02-11	Moved Order_Relation into Library and moved some of it into Relation.	file \| diff \| annotate
2009-01-21	haftmann	2009-01-21	changed import hierarchy	file \| diff \| annotate
2008-08-26	krauss	2008-08-26	added distributivity of relation composition over union [simp]	file \| diff \| annotate
2008-03-17	nipkow	2008-03-17	added lemmas	file \| diff \| annotate
2008-03-14	nipkow	2008-03-14	Added lemmas	file \| diff \| annotate
2007-10-08	haftmann	2007-10-08	integrated FixedPoint into Inductive	file \| diff \| annotate
2007-08-15	paulson	2007-08-15	ATP blacklisting is now in theory data, attribute noatp	file \| diff \| annotate
2007-07-10	haftmann	2007-07-10	moved lfp_induct2 here	file \| diff \| annotate
2007-06-01	krauss	2007-06-01	Added simp-rules: "R O {} = {}" and "{} O R = {}"	file \| diff \| annotate
2007-01-24	paulson	2007-01-24	some new 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-26	krauss	2006-09-26	Changed precedence of "op O" (relation composition) from 60 to 75.	file \| diff \| annotate
2006-05-16	wenzelm	2006-05-16	tuned concrete syntax -- abbreviation/const_syntax;	file \| diff \| annotate
2006-04-08	wenzelm	2006-04-08	refined 'abbreviation';	file \| diff \| annotate
2006-03-23	nipkow	2006-03-23	Converted translations to abbbreviations. Removed a few odd functions from Map and AssocList. Moved chg_map from Map to Bali/Basis.	file \| diff \| annotate
2006-03-10	huffman	2006-03-10	added many simple lemmas	file \| diff \| annotate
2005-09-22	nipkow	2005-09-22	renamed rules to iprover	file \| diff \| annotate
2004-09-03	paulson	2004-09-03	new theorem symD	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
2003-02-26	paulson	2003-02-26	some x-symbols and some new lemmas	file \| diff \| annotate
2003-02-08	paulson	2003-02-08	converting HOL/UNITY to use unconditional fairness	file \| diff \| annotate
2002-10-10	berghofe	2002-10-10	Removed obsolete function "fun_rel_comp".	file \| diff \| annotate
2002-08-30	paulson	2002-08-30	removal of blast.overloaded	file \| diff \| annotate

isabelle

RSS Atom