src/FOL/simpdata.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;
Thu, 13 Jul 2000 12:56:42 +0200 paulson AddIffs now available for FOL, ZF
Fri, 31 Mar 2000 22:22:23 +0200 wenzelm added cong atts;
Wed, 15 Mar 2000 18:42:54 +0100 wenzelm clasimp: include Splitter;
Tue, 21 Sep 1999 19:11:07 +0200 nipkow Mod because of new solver interface.
Wed, 25 Aug 1999 20:45:19 +0200 wenzelm proper bootstrap of IFOL/FOL theories and packages;
Wed, 17 Mar 1999 16:33:47 +0100 wenzelm Theory.sign_of;
Wed, 13 Jan 1999 12:08:51 +0100 paulson congruence rules finally use == instead of = and <->
Thu, 24 Sep 1998 17:18:33 +0200 oheimb simplified CLASIMP_DATA
Fri, 18 Sep 1998 14:34:06 +0200 paulson Pruning of parameters and True assumptions
Wed, 12 Aug 1998 17:40:18 +0200 oheimb minor adaption for SML/NJ
Wed, 12 Aug 1998 16:21:18 +0200 oheimb the splitter is now defined as a functor
Thu, 30 Jul 1998 19:18:50 +0200 wenzelm made SML/NJ happy;
Thu, 30 Jul 1998 19:02:52 +0200 wenzelm functorized Clasimp module;
Thu, 02 Jul 1998 17:56:06 +0200 paulson HACKED declaration of addsplits
Thu, 14 May 1998 16:50:09 +0200 oheimb extended addsplits and delsplits to handle also split rules for assumptions
Sat, 04 Apr 1998 12:29:07 +0200 wenzelm no open Simplifier;
Sat, 28 Feb 1998 15:41:17 +0100 nipkow Splitters via named loopers.
Wed, 25 Feb 1998 20:25:27 +0100 oheimb factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning
Wed, 25 Feb 1998 15:45:32 +0100 oheimb changed wrapper mechanism of classical reasoner
Wed, 24 Dec 1997 10:02:30 +0100 paulson New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
Wed, 03 Dec 1997 10:48:16 +0100 paulson Instantiated the one-point-rule quantifier simpprocs for FOL
Fri, 28 Nov 1997 10:54:13 +0100 paulson addsplits now in FOL, ZF too
Wed, 12 Nov 1997 12:23:37 +0100 oheimb renamed split_prem_tac to split_asm_tac
Fri, 07 Nov 1997 18:05:25 +0100 oheimb added split_prem_tac
Fri, 07 Nov 1997 18:02:15 +0100 oheimb changed libraray function find to find_index_eq, currying it
Mon, 03 Nov 1997 12:28:01 +0100 wenzelm adapted to new implicit simpset;
Fri, 17 Oct 1997 10:57:48 +0200 paulson New simprules imp_disj1,2 and some comments
Fri, 10 Oct 1997 15:52:12 +0200 wenzelm fixed dots;
Wed, 06 Aug 1997 00:41:40 +0200 berghofe Moved functions from file "thy_data.ML".
Wed, 23 Jul 1997 12:54:49 +0200 wenzelm standard congs;
Tue, 22 Jul 1997 11:12:55 +0200 paulson Removal of the tactical STATE
Thu, 15 May 1997 15:51:09 +0200 oheimb renamed addss to addSss, unsafe_addss to addss, extended auto_tac
Tue, 18 Mar 1997 08:43:26 +0100 nipkow Added P&P&Q <-> P&Q and P|P|Q <-> P|Q
Wed, 05 Mar 1997 10:07:04 +0100 paulson Eta-expanded declarations of addSIs2, etc., to avoid polymorphism errors
Sat, 15 Feb 1997 17:43:27 +0100 oheimb added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss,
Mon, 10 Feb 1997 12:31:54 +0100 paulson Renamed structure Int (intuitionistic prover) to IntPr to prevent clash
less more (0) -60 tip