src/ZF/func.ML
Thu, 15 Nov 2001 17:59:56 +0100 paulson miniscoping of UN and INT
Thu, 07 Sep 2000 21:12:49 +0200 wenzelm tuned ML code (the_context, bind_thms(s));
Thu, 24 Aug 2000 11:05:20 +0200 paulson added some xsymbols, and tidied
Fri, 30 Jun 2000 12:51:30 +0200 paulson removal of batch-style proofs
Wed, 28 Jun 2000 10:56:34 +0200 paulson fixed some weak elim rules
Mon, 07 Feb 2000 15:14:02 +0100 paulson tidied some proofs
Wed, 02 Feb 2000 12:25:29 +0100 paulson new lemma fun_cons_restrict_eq
Mon, 31 Jan 2000 16:13:28 +0100 paulson Pi_empty1 is a more general simprule than empty_fun
Thu, 13 Jan 2000 17:36:58 +0100 paulson new lemmas for Ntree recursor example; more simprules; more lemmas borrowed
Tue, 07 Sep 1999 10:40:58 +0200 wenzelm isatool expandshort;
Wed, 27 Jan 1999 10:31:31 +0100 paulson new typechecking solver for the simplifier
Fri, 18 Sep 1998 15:09:46 +0200 paulson tidied
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
Mon, 27 Jul 1998 16:04:20 +0200 paulson A few new lemmas by Mark Staples
Fri, 17 Jul 1998 11:13:43 +0200 paulson A stronger apply_0, and new thm domain_lam
Mon, 13 Jul 1998 16:43:57 +0200 paulson Huge tidy-up: removal of leading \!\!
Mon, 22 Jun 1998 17:12:27 +0200 wenzelm isatool fixgoal;
Mon, 27 Apr 1998 13:47:46 +0200 paulson New proof of apply_equality and new thm Pi_image_cons
Fri, 02 Jan 1998 17:17:24 +0100 paulson Changed required by new blast_tac (the one that squashes flex-flex pairs)
Mon, 03 Nov 1997 12:24:13 +0100 wenzelm isatool fixclasimp;
Fri, 10 Oct 1997 18:23:31 +0200 wenzelm fixed dots;
Fri, 02 May 1997 10:19:19 +0200 paulson Higher bound means much faster proof
Mon, 21 Apr 1997 10:16:41 +0200 paulson Moved blast_tac demo from ZF/func.ML to ZF/ex/misc.ML
Tue, 15 Apr 1997 10:23:17 +0200 paulson Addition of blast_tac benchmark
Wed, 09 Apr 1997 12:37:44 +0200 paulson Using Blast_tac
Fri, 04 Apr 1997 11:32:44 +0200 paulson Simplified a proof
Wed, 02 Apr 1997 15:39:44 +0200 paulson Converted to call blast_tac.
Mon, 24 Mar 1997 10:28:23 +0100 paulson Deleted needless parentheses
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
Thu, 26 Sep 1996 15:14:23 +0200 paulson Ran expandshort; used stac instead of ssubst
Tue, 30 Jan 1996 13:42:57 +0100 clasohm expanded tabs
Thu, 12 Jan 1995 03:03:45 +0100 lcp Renamed single_fun to singleton_fun.
Fri, 23 Dec 1994 16:27:07 +0100 lcp empty_fun: generalized from -> to Pi
Wed, 07 Dec 1994 13:12:04 +0100 clasohm added qed and qed_goal[w]
Thu, 24 Nov 1994 10:23:41 +0100 lcp cons_fun_eq: modified strange uses of classical reasoner
Thu, 03 Nov 1994 12:39:39 +0100 lcp ZF/func: tidied many proofs, using new definition of Pi(A,B)
Wed, 17 Aug 1994 10:33:23 +0200 lcp ZF/func/fun_extend3: new
Mon, 15 Aug 1994 18:04:10 +0200 lcp ZF/func/empty_fun: renamed from fun_empty
Fri, 12 Aug 1994 18:45:33 +0200 lcp for infinite datatypes with arbitrary index sets
Tue, 26 Jul 1994 13:44:42 +0200 lcp Axiom of choice, cardinality results, etc.
Thu, 23 Jun 1994 17:38:12 +0200 lcp modifications for cardinal arithmetic
Tue, 21 Jun 1994 17:20:34 +0200 lcp Addition of cardinals and order types, various tidying
Fri, 19 Nov 1993 11:25:36 +0100 lcp expandshort and other trivial changes
Thu, 07 Oct 1993 10:48:16 +0100 lcp added ~: for "not in"
Thu, 30 Sep 1993 10:10:21 +0100 lcp ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
Fri, 17 Sep 1993 16:16:38 +0200 lcp Installation of new simplifier for ZF. Deleted all congruence rules not
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip