src/HOL/Relation.thy
2013-10-18 blanchet 2013-10-18 killed most "no_atp", to make Sledgehammer more complete
2013-09-17 nipkow 2013-09-17 added lemmas and made concerse executable
2013-07-28 traytel 2013-07-28 more converse(p) theorems; tuned proofs;
2013-07-25 traytel 2013-07-25 two useful relation theorems
2013-06-19 nipkow 2013-06-19 added lemma
2012-12-07 nipkow 2012-12-07 corrected nonsensical associativity of `` and dvd
2012-07-31 kuncar 2012-07-31 more relation operations expressed by Finite_Set.fold
2012-07-12 bulwahn 2012-07-12 a first guess to avoid the Codegenerator_Test to loop infinitely
2012-05-16 kuncar 2012-05-16 generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
2012-04-12 bulwahn 2012-04-12 merged
2012-04-03 griff 2012-04-03 dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
2012-04-03 griff 2012-04-03 renamed "rel_comp" to "relcomp" (to be consistent with, e.g., "relpow")
2012-04-05 huffman 2012-04-05 define reflp directly, in the manner of symp and transp
2012-03-22 haftmann 2012-03-22 fixed typo
2012-03-17 haftmann 2012-03-17 spelt out missing colemmas
2012-03-17 haftmann 2012-03-17 generalized INF_INT_eq, SUP_UN_eq
2012-03-12 noschinl 2012-03-12 tuned proofs
2012-03-12 noschinl 2012-03-12 tuned pred_set_conv lemmas. Skipped lemmas changing the lemmas generated by inductive_set
2012-03-12 noschinl 2012-03-12 tuned simpset
2012-03-07 haftmann 2012-03-07 tuned syntax; more candidates
2012-03-02 haftmann 2012-03-02 more fundamental pred-to-set conversions for range and domain by means of inductive_set
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)
2012-02-26 haftmann 2012-02-26 restored accidental omission
2012-02-26 haftmann 2012-02-26 tuned structure
2012-02-26 haftmann 2012-02-26 tuned structure; dropped already existing syntax declarations
2012-02-26 haftmann 2012-02-26 tuned syntax declarations; tuned structure
2012-02-26 haftmann 2012-02-26 marked candidates for rule declarations
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
2012-02-24 haftmann 2012-02-24 given up disfruitful branch
2012-02-24 haftmann 2012-02-24 explicit remove of lattice notation
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
2012-01-30 nipkow 2012-01-30 added "'a rel"
2012-01-01 haftmann 2012-01-01 cleanup of code declarations
2011-12-24 haftmann 2011-12-24 dropped obsolete code equation for Id
2011-10-13 haftmann 2011-10-13 moved acyclic predicate up in hierarchy
2011-10-13 haftmann 2011-10-13 modernized definitions
2011-09-20 haftmann 2011-09-20 tuned specification and lemma distribution among theories; tuned proofs
2011-09-13 huffman 2011-09-13 tuned proofs
2011-08-18 haftmann 2011-08-18 observe distinction between sets and predicates more properly
2011-02-21 blanchet 2011-02-21 renamed "nitpick\_def" to "nitpick_unfold" to reflect its new semantics
2010-12-07 bulwahn 2010-12-07 adding a definition for refl_on which is friendly for quickcheck and nitpick
2010-12-03 bulwahn 2010-12-03 adding a nice definition of Id_on for quickcheck and nitpick
2010-05-09 krauss 2010-05-09 added lemmas rel_comp_UNION_distrib(2)
2010-05-07 krauss 2010-05-07 removed semicolons
2010-05-07 krauss 2010-05-07 rule subrelI (for nice Isar proofs of relation inequalities)
2010-03-18 blanchet 2010-03-18 now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"
2009-10-26 krauss 2009-10-26 lemma converse_inv_image
2009-10-05 paulson 2009-10-05 New facts about domain and range in
2009-10-01 haftmann 2009-10-01 proper merge of interpretation equations
2009-08-31 krauss 2009-08-31 moved lemma Wellfounded.in_inv_image to Relation.thy
2009-07-27 krauss 2009-07-27 "more standard" argument order of relation composition (op O)
2009-04-28 haftmann 2009-04-28 ephermal enforcement of import order to circumvent current problem in merging interpretation morphisms
2009-03-02 nipkow 2009-03-02 name changes
2009-02-11 nipkow 2009-02-11 Moved Order_Relation into Library and moved some of it into Relation.
2009-01-21 haftmann 2009-01-21 changed import hierarchy
2008-08-26 krauss 2008-08-26 added distributivity of relation composition over union [simp]
2008-03-17 nipkow 2008-03-17 added lemmas
2008-03-14 nipkow 2008-03-14 Added lemmas
2007-10-08 haftmann 2007-10-08 integrated FixedPoint into Inductive
2007-08-15 paulson 2007-08-15 ATP blacklisting is now in theory data, attribute noatp