src/FOL/simpdata.ML
Fri, 27 Apr 2007 16:31:20 +0200 wenzelm removed obsolete induct/simp tactic;
Sat, 20 Jan 2007 14:09:11 +0100 wenzelm added @{clasimpset};
Sun, 26 Nov 2006 23:43:53 +0100 wenzelm converted legacy ML scripts;
Thu, 27 Jul 2006 13:43:00 +0200 wenzelm tuned proofs;
Thu, 19 Jan 2006 21:22:08 +0100 wenzelm setup: theory -> theory;
Sat, 31 Dec 2005 21:49:36 +0100 wenzelm removed obsolete Provers/make_elim.ML;
Thu, 01 Dec 2005 22:03:01 +0100 wenzelm unfold_tac: static evaluation of simpset;
Tue, 18 Oct 2005 17:59:25 +0200 wenzelm Simplifier.theory_context;
Mon, 17 Oct 2005 23:10:10 +0200 wenzelm change_claset/simpset;
Mon, 12 Sep 2005 18:20:32 +0200 haftmann introduced new-style AList operations
Tue, 02 Aug 2005 19:47:12 +0200 wenzelm simprocs: Simplifier.inherit_bounds;
Sun, 22 May 2005 16:51:07 +0200 wenzelm Simplifier already setup in Pure;
Thu, 03 Mar 2005 12:43:01 +0100 skalberg Move towards standard functions.
Sun, 13 Feb 2005 17:15:14 +0100 skalberg Deleted Library.option type.
Tue, 06 Aug 2002 11:22:05 +0200 wenzelm sane interface for simprocs;
Wed, 15 May 2002 10:42:32 +0200 paulson better simplification of trivial existential equalities
Mon, 21 Jan 2002 14:47:55 +0100 paulson new simprules and classical rules
Tue, 15 Jan 2002 15:07:41 +0100 paulson new theorem
Sat, 12 Jan 2002 16:37:58 +0100 wenzelm renamed forall_elim_vars_safe to gen_all;
Fri, 11 Jan 2002 14:53:30 +0100 wenzelm replace gen_all by forall_elim_vars_safe;
Mon, 17 Dec 2001 14:27:18 +0100 nipkow mods due to changed 1-point simprocs (quantifier1).
Sat, 03 Nov 2001 18:42:38 +0100 wenzelm proper use of bind_thm(s);
Sun, 14 Oct 2001 22:15:07 +0200 wenzelm moved rulify to ObjectLogic;
Sun, 14 Oct 2001 19:59:55 +0200 wenzelm eliminated atomize rules;
Thu, 31 May 2001 16:52:02 +0200 oheimb streamlined addIffs/delIffs, added warnings
Thu, 29 Mar 2001 13:59:54 +0200 nipkow generalization of 1 point rules for ALL
Fri, 10 Nov 2000 19:01:33 +0100 wenzelm FOL_basic_ss: simprocs moved to FOL_ss;
Thu, 07 Sep 2000 20:49:19 +0200 wenzelm rulify setup;
Tue, 05 Sep 2000 18:46:36 +0200 wenzelm iff declarations moved to clasimp.ML;
Tue, 29 Aug 2000 00:55:31 +0200 wenzelm cong setup now part of Simplifier;
less more (0) -50 -30 tip