src/HOL/Relation.thy
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
2007-07-10 haftmann 2007-07-10 moved lfp_induct2 here
2007-06-01 krauss 2007-06-01 Added simp-rules: "R O {} = {}" and "{} O R = {}"
2007-01-24 paulson 2007-01-24 some new lemmas
2006-11-17 wenzelm 2006-11-17 more robust syntax for definition/abbreviation/notation;
2006-11-07 wenzelm 2006-11-07 renamed 'const_syntax' to 'notation';
2006-09-26 krauss 2006-09-26 Changed precedence of "op O" (relation composition) from 60 to 75.
2006-05-16 wenzelm 2006-05-16 tuned concrete syntax -- abbreviation/const_syntax;
2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
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.
2006-03-10 huffman 2006-03-10 added many simple lemmas
2005-09-22 nipkow 2005-09-22 renamed rules to iprover
2004-09-03 paulson 2004-09-03 new theorem symD
2004-08-18 nipkow 2004-08-18 import -> imports
2004-08-16 nipkow 2004-08-16 New theory header syntax.
2003-02-26 paulson 2003-02-26 some x-symbols and some new lemmas
2003-02-08 paulson 2003-02-08 converting HOL/UNITY to use unconditional fairness
2002-10-10 berghofe 2002-10-10 Removed obsolete function "fun_rel_comp".
2002-08-30 paulson 2002-08-30 removal of blast.overloaded
2002-07-11 nipkow 2002-07-11 *** empty log message ***
2002-02-21 wenzelm 2002-02-21 fixed document; tuned;
2002-02-20 berghofe 2002-02-20 Converted to new theory format.
2001-12-13 nipkow 2001-12-13 comp -> rel_comp
2001-02-15 oheimb 2001-02-15 moved inv_image to Relation
2001-01-09 nipkow 2001-01-09 `` -> and ``` -> ``
2001-01-05 nipkow 2001-01-05 ^^ -> ``` Univalent -> single_valued
2001-01-05 paulson 2001-01-05 Field of a relation, and some Domain/Range rules
2000-10-30 wenzelm 2000-10-30 converse: syntax \<inverse>;
2000-10-12 nipkow 2000-10-12 *** empty log message ***
2000-04-13 nipkow 2000-04-13 Times -> <*> ** -> <*lex*>
2000-02-21 oheimb 2000-02-21 renamed Univalent to univalent
1999-10-22 paulson 1999-10-22 tidied using modern infix form
1999-07-16 berghofe 1999-07-16 Added some definitions and theorems needed for the construction of datatypes involving function types.
1999-06-10 paulson 1999-06-10 new preficates refl, sym [from Integ/Equiv], antisym
1998-11-27 paulson 1998-11-27 moved diag (diagonal relation) from Univ to Relation
1998-10-02 nipkow 1998-10-02 id <-> Id
1998-03-16 paulson 1998-03-16 inverse -> converse [It is standard terminology and also used in ZF]
1998-01-08 oheimb 1998-01-08 added Univalent
1997-07-04 nipkow 1997-07-04 Reduced priority of postfix ^* etc operators such that they are the same as application. Eg wf r^* now needs to be written wf(r^*).