src/ZF/List.ML
Wed, 15 May 2002 10:42:32 +0200 paulson better simplification of trivial existential equalities
Mon, 13 May 2002 13:22:01 +0200 paulson Deleting two simprules saves 21 seconds!
Mon, 21 Jan 2002 14:47:55 +0100 paulson new simprules and classical rules
Thu, 17 Jan 2002 12:45:52 +0100 paulson new definitions from Sidi Ehmety
Thu, 15 Feb 2001 17:18:54 +0100 wenzelm eliminate get_def; Isabelle99-2
Thu, 07 Sep 2000 21:12:49 +0200 wenzelm tuned ML code (the_context, bind_thms(s));
Mon, 07 Aug 2000 10:29:54 +0200 paulson instantiated Cancel_Numerals for "nat" in ZF
Tue, 01 Aug 2000 15:28:21 +0200 paulson natify, a coercion to reduce the number of type constraints in arithmetic
Wed, 27 Jan 1999 10:31:31 +0100 paulson new typechecking solver for the simplifier
Tue, 19 Jan 1999 11:18:11 +0100 paulson removal of the (thm list) argument of mk_cases
Wed, 13 Jan 1999 11:57:09 +0100 paulson datatype package improvements
Thu, 07 Jan 1999 18:30:55 +0100 paulson ZF: the natural numbers as a datatype
Wed, 06 Jan 1999 13:24:33 +0100 paulson induct_tac and exhaust_tac
Mon, 28 Dec 1998 16:59:28 +0100 paulson new inductive, datatype and primrec packages, etc.
Tue, 22 Sep 1998 13:50:57 +0200 paulson tidying
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
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, 03 Nov 1997 12:24:13 +0100 wenzelm isatool fixclasimp;
Fri, 10 Oct 1997 18:23:31 +0200 wenzelm fixed dots;
Wed, 23 Apr 1997 10:54:22 +0200 paulson Conversion to use blast_tac
Sat, 15 Feb 1997 17:52:31 +0100 oheimb reflecting my recent changes of the simplifier and classical reasoner
Thu, 09 Jan 1997 10:20:03 +0100 paulson Removal of needless "addIs [equality]", etc.
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, 20 Aug 1996 12:36:58 +0200 paulson Addition of function set_of_list
Thu, 18 Apr 1996 14:43:00 +0200 oheimb adapted proof of drop_succ_Cons: problem with non-confluent simpset removed
Tue, 30 Jan 1996 13:42:57 +0100 clasohm expanded tabs
Mon, 27 Feb 1995 17:40:57 +0100 lcp Updated comment about list_subset_univ and list_into_univ.
Wed, 14 Dec 1994 11:41:49 +0100 clasohm added bind_thm for theorems defined by "standard ..."
Wed, 07 Dec 1994 13:12:04 +0100 clasohm added qed and qed_goal[w]
Mon, 15 Aug 1994 18:25:27 +0200 lcp ZF/List, ex/Brouwer,Data,LList,Ntree,TF,Term: much simplified proof of _unfold
Fri, 12 Aug 1994 12:51:34 +0200 lcp installation of new inductive/datatype sections
Tue, 26 Jul 1994 13:21:20 +0200 lcp Axiom of choice, cardinality results, etc.
Fri, 15 Jul 1994 13:34:31 +0200 clasohm added thy_name to Datatype_Fun's parameter
Fri, 01 Jul 1994 11:03:42 +0200 clasohm replaced extend_theory by new add_* functions;
Tue, 21 Jun 1994 17:20:34 +0200 lcp Addition of cardinals and order types, various tidying
Thu, 17 Mar 1994 12:36:58 +0100 lcp Improved layout for inductive defs
Tue, 16 Nov 1993 14:24:21 +0100 clasohm made pseudo theories for all ML files;
Thu, 28 Oct 1993 11:30:35 +0100 lcp now uses datatype_intrs and datatype_elims
Fri, 22 Oct 1993 11:34:41 +0100 lcp ZF/ind-syntax/fold_con_tac: deleted, since fold_tac now works
Fri, 15 Oct 1993 10:21:01 +0100 lcp ZF/ind-syntax/refl_thin: new
Wed, 06 Oct 1993 09:58:53 +0100 lcp Retrying yet again after network problems
Thu, 30 Sep 1993 10:26:38 +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