src/HOL/Relation.ML
Wed, 11 Mar 1998 11:05:14 +0100 paulson New theorem Image_eq_UN; deleted the silly vimage_inverse_Image
Tue, 03 Mar 1998 15:12:25 +0100 paulson New theorems; tidied
Wed, 25 Feb 1998 15:48:04 +0100 oheimb added split_all_tac to claset()
Mon, 23 Feb 1998 11:15:40 +0100 paulson New laws for id
Thu, 05 Feb 1998 10:48:43 +0100 paulson New theorem Image_id
Mon, 02 Feb 1998 12:55:39 +0100 paulson Three new facts about Image
Tue, 16 Dec 1997 17:58:03 +0100 wenzelm expandshort;
Mon, 03 Nov 1997 12:13:18 +0100 wenzelm isatool fixclasimp;
Fri, 26 Sep 1997 10:21:14 +0200 paulson Minor tidying to use Clarify_tac, etc.
Tue, 17 Jun 1997 09:01:56 +0200 nipkow converse -> ^-1
Thu, 05 Jun 1997 14:39:22 +0200 nipkow Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'.
Fri, 04 Apr 1997 11:18:52 +0200 paulson Calls Blast_tac
Sat, 15 Feb 1997 17:52:31 +0100 oheimb reflecting my recent changes of the simplifier and classical reasoner
Thu, 26 Sep 1996 12:47:47 +0200 paulson Ran expandshort
Thu, 12 Sep 1996 10:40:05 +0200 paulson Tidied many proofs, using AddIffs to let equivalences take
Fri, 28 Jun 1996 15:29:05 +0200 paulson Removed the unused rel_eq_cs
Mon, 03 Jun 1996 17:10:56 +0200 berghofe best_tac, deepen_tac and safe_tac now also use default claset.
Thu, 23 May 1996 15:15:20 +0200 berghofe Removed equalityI from some proofs (because it is now included
Tue, 21 May 1996 13:39:31 +0200 berghofe Replaced fast_tac by Fast_tac (which uses default claset)
Sat, 27 Apr 1996 12:07:31 +0200 nipkow Added R_O_id and id_O_R
Thu, 04 Apr 1996 11:45:01 +0200 paulson Using new "Times" infix
Mon, 25 Mar 1996 11:13:59 +0100 nipkow added converse_converse
Wed, 06 Mar 1996 12:52:11 +0100 paulson Ran expandshort
Tue, 30 Jan 1996 15:24:36 +0100 clasohm expanded tabs
Fri, 26 Jan 1996 20:25:39 +0100 nipkow Streamlined defs in Relation and added new intro/elim rules to do with
Wed, 04 Oct 1995 13:10:03 +0100 clasohm added local simpsets; removed IOA from 'make test'
Fri, 26 May 1995 18:11:47 +0200 nipkow Trancl is now based on Relation which used to be in Integ.
less more (0) tip