src/HOL/Relation.thy
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^*).
1997-06-17 nipkow 1997-06-17 converse -> ^-1
1996-09-12 paulson 1996-09-12 Simplification and tidying of definitions
1996-04-27 nipkow 1996-04-27 Generalized types of some of the operators (thanks to Norbert Voelker)
1996-02-05 clasohm 1996-02-05 expanded tabs; renamed subtype to typedef; incorporated Konrad's changes
1996-01-26 nipkow 1996-01-26 Streamlined defs in Relation and added new intro/elim rules to do with pattern matching in sets: {(x,y). ...} and UN (x,y):A. ...
1995-05-26 nipkow 1995-05-26 Trancl is now based on Relation which used to be in Integ.