src/ZF/equalities.ML
Fri, 15 Feb 2002 12:07:27 +0100 paulson a new definition of "restrict"
Thu, 15 Nov 2001 17:59:56 +0100 paulson miniscoping of UN and INT
Fri, 05 Oct 2001 21:37:33 +0200 wenzelm sane spacing of "-";
Thu, 07 Sep 2000 21:12:49 +0200 wenzelm tuned ML code (the_context, bind_thms(s));
Thu, 13 Jul 2000 13:02:20 +0200 paulson fixed a failing proof
Wed, 28 Jun 2000 12:34:08 +0200 paulson tidying and unbatchifying
Wed, 03 Mar 1999 10:36:24 +0100 paulson expandshort
Mon, 22 Feb 1999 10:19:32 +0100 paulson new theorems Pow_0 and Pow_insert; renamed other Pow theorems
Thu, 07 Jan 1999 10:56:05 +0100 paulson if-then-else syntax for ZF
Mon, 17 Aug 1998 13:09:08 +0200 paulson Yet more removal of "goal" commands, especially "goal ZF.thy", so ZF.thy
Fri, 14 Aug 1998 18:37:28 +0200 paulson got rid of some goal thy commands
Wed, 15 Jul 1998 14:13:18 +0200 paulson More tidying and removal of "\!\!... from Goal commands
Thu, 02 Jul 1998 17:58:12 +0200 paulson Renamed expand_if to split_if and setloop split_tac to addsplits,
Mon, 22 Jun 1998 17:12:27 +0200 wenzelm isatool fixgoal;
Tue, 28 Apr 1998 13:51:39 +0200 paulson new thms image_0_left, image_Un_left, etc.
Fri, 27 Feb 1998 11:06:28 +0100 paulson New vimage laws
Thu, 20 Nov 1997 11:03:26 +0100 paulson Two new rewrites
Mon, 03 Nov 1997 12:24:13 +0100 wenzelm isatool fixclasimp;
Wed, 09 Apr 1997 12:37:44 +0200 paulson Using Blast_tac
Wed, 02 Apr 1997 15:39:44 +0200 paulson Converted to call blast_tac.
Wed, 08 Jan 1997 15:04:27 +0100 paulson Removal of sum_cs and eq_cs
Fri, 03 Jan 1997 15:01:55 +0100 paulson Implicit simpsets and clasets for FOL and ZF
Mon, 03 Jun 1996 11:43:55 +0200 paulson Added a new theorem, UN_Int_subset
Thu, 04 Apr 1996 18:18:48 +0200 paulson Proved Inter_0 and converse_INT
Tue, 26 Mar 1996 11:50:40 +0100 paulson New results from AC/Cardinal_aux.ML
Mon, 11 Mar 1996 14:19:12 +0100 paulson New theorem: Inter_Un_subset
Tue, 30 Jan 1996 13:42:57 +0100 clasohm expanded tabs
Fri, 14 Apr 1995 11:24:51 +0200 lcp Renamed domain_diff_subset, range_diff_subset,
Thu, 13 Apr 1995 11:37:39 +0200 lcp Proved Int_Diff_eq.
Fri, 23 Dec 1994 16:51:10 +0100 lcp RepFun_eq_0_iff, RepFun_0: new
less more (0) -30 tip