src/FOL/simpdata.ML
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
Fri, 03 Jan 1997 15:01:55 +0100 paulson Implicit simpsets and clasets for FOL and ZF
Wed, 09 Oct 1996 13:36:17 +0200 paulson Added the de Morgan laws (incl quantifier versions) to basic simpset
Tue, 08 Oct 1996 10:17:50 +0200 paulson Addition of one-point quantifier rewrite rules
Mon, 09 Sep 1996 10:59:32 +0200 paulson Removal of (EX x. P) <-> P and (ALL x. P) <-> P
Thu, 05 Sep 1996 18:28:01 +0200 paulson Introduction of miniscoping for FOL
Mon, 19 Aug 1996 11:20:37 +0200 paulson Added a lot of basic laws, from HOL/simpdata
Mon, 06 May 1996 15:21:05 +0200 berghofe Added split_inside_tac.
Mon, 29 Jan 1996 13:58:15 +0100 clasohm expanded tabs
Wed, 03 May 1995 13:35:09 +0200 lcp Imported meta_eq_to_obj_eq from HOL for use with 'split'.
Thu, 30 Mar 1995 13:36:00 +0200 lcp Defined addss to perform simplification in a claset.
Wed, 08 Mar 1995 14:01:08 +0100 nipkow Enforced partial evaluation of mk_case_split_tac.
Wed, 14 Dec 1994 16:48:36 +0100 lcp conj_commute,disj_commute: new
Wed, 30 Nov 1994 13:18:42 +0100 clasohm added qed_goal for meta_iffD
Fri, 25 Nov 1994 00:02:37 +0100 lcp added blank line
Fri, 17 Jun 1994 17:49:03 +0200 lcp atomize: borrowed HOL version, which checks for both Trueprop
Tue, 24 May 1994 09:04:03 +0200 nipkow Modified mk_meta_eq to leave meta-equlities on unchanged.
Fri, 13 May 1994 11:25:55 +0200 lcp FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the
Thu, 17 Mar 1994 13:54:50 +0100 lcp FOL/simpdata: tidied
Wed, 05 Jan 1994 19:41:37 +0100 nipkow updated solver of FOL_ss. see change of HOL/simpdata.ML
Tue, 12 Oct 1993 13:39:35 +0100 nipkow Added gen_all to simpdata.ML.
Thu, 16 Sep 1993 16:55:17 +0200 nipkow defined local addcongs
Thu, 16 Sep 1993 12:20:38 +0200 clasohm Initial revision
less more (0) tip