src/HOL/Relation.ML
2002-10-10 berghofe 2002-10-10 Removed obsolete function "fun_rel_comp".
2002-02-20 berghofe 2002-02-20 Converted to new theory format.
2001-12-13 nipkow 2001-12-13 comp -> rel_comp
2001-10-03 wenzelm 2001-10-03 tuned parentheses in relational expressions;
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
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-09-15 paulson 2000-09-15 renamed (most of...) the select rules
2000-06-23 paulson 2000-06-23 new theorem trans_O_subset
2000-06-22 wenzelm 2000-06-22 bind_thm(s);
2000-06-21 paulson 2000-06-21 generalized {Domain,Range}_partial_func to {Domain,Range}_Collect_split
2000-04-13 nipkow 2000-04-13 Times -> <*> ** -> <*lex*>
2000-02-21 oheimb 2000-02-21 renamed Univalent to univalent
2000-02-21 nipkow 2000-02-21 A few lemmas and some Adds.
2000-01-31 paulson 2000-01-31 new theorem rev_ImageI
1999-11-11 paulson 1999-11-11 Fixed obsolete use of "op ^^"; new lemma
1999-10-22 paulson 1999-10-22 new theorems on Image
1999-10-11 paulson 1999-10-11 new thm Domain_mono
1999-07-26 paulson 1999-07-26 three new theorems
1999-07-19 paulson 1999-07-19 getting rid of qed_goal
1999-07-16 berghofe 1999-07-16 Added some definitions and theorems needed for the construction of datatypes involving function types.
1999-07-15 paulson 1999-07-15 qed_goal -> Goal
1999-06-10 paulson 1999-06-10 new preficates refl, sym [from Integ/Equiv], antisym
1998-12-02 paulson 1998-12-02 new theorems Domain_Union, Range_Union
1998-12-01 paulson 1998-12-01 better version of Image_diag
1998-11-30 paulson 1998-11-30 new theorems about diag
1998-11-27 paulson 1998-11-27 moved diag (diagonal relation) from Univ to Relation
1998-11-09 paulson 1998-11-09 new Domain/Range rules
1998-10-15 paulson 1998-10-15 Uses overload_1st_set to specify overloading
1998-10-02 nipkow 1998-10-02 id <-> Id
1998-08-19 paulson 1998-08-19 Overloading decl should assist Blast_tac
1998-08-13 paulson 1998-08-13 even more tidying of Goal commands
1998-07-31 paulson 1998-07-31 new theorems for partial funcs
1998-07-15 paulson 1998-07-15 More tidying and removal of "\!\!... from Goal commands
1998-07-15 paulson 1998-07-15 Removal of leading "\!\!..." from most Goal commands
1998-06-22 wenzelm 1998-06-22 isatool fixgoal;
1998-04-27 nipkow 1998-04-27 Added a few lemmas. Renamed expand_const -> split_const.
1998-03-30 oheimb 1998-03-30 added introduction and elimination rules for Univalent
1998-03-16 paulson 1998-03-16 inverse -> converse [It is standard terminology and also used in ZF]
1998-03-11 paulson 1998-03-11 New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
1998-03-03 paulson 1998-03-03 New theorems; tidied
1998-02-25 oheimb 1998-02-25 added split_all_tac to claset()
1998-02-23 paulson 1998-02-23 New laws for id
1998-02-05 paulson 1998-02-05 New theorem Image_id
1998-02-02 paulson 1998-02-02 Three new facts about Image
1997-12-16 wenzelm 1997-12-16 expandshort;
1997-11-03 wenzelm 1997-11-03 isatool fixclasimp;
1997-09-26 paulson 1997-09-26 Minor tidying to use Clarify_tac, etc.
1997-06-17 nipkow 1997-06-17 converse -> ^-1
1997-06-05 nipkow 1997-06-05 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. Relation.ML Trancl.ML: more thms WF.ML WF.thy: added `acyclic' WF_Rel.ML: moved some thms back into WF and added some new ones.
1997-04-04 paulson 1997-04-04 Calls Blast_tac
1997-02-15 oheimb 1997-02-15 reflecting my recent changes of the simplifier and classical reasoner
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-12 paulson 1996-09-12 Tidied many proofs, using AddIffs to let equivalences take the place of separate Intr and Elim rules. Also deleted most named clasets.
1996-06-28 paulson 1996-06-28 Removed the unused rel_eq_cs
1996-06-03 berghofe 1996-06-03 best_tac, deepen_tac and safe_tac now also use default claset.
1996-05-23 berghofe 1996-05-23 Removed equalityI from some proofs (because it is now included in the default claset)
1996-05-21 berghofe 1996-05-21 Replaced fast_tac by Fast_tac (which uses default claset) New rules are now also added to default claset.