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.