src/FOL/simpdata.ML
1998-08-12 oheimb 1998-08-12 minor adaption for SML/NJ
1998-08-12 oheimb 1998-08-12 the splitter is now defined as a functor moved addsplits, delsplits, Addsplits, Delsplits to Provers/splitter.ML moved split_thm_info to Provers/splitter.ML definined atomize via general mk_atomize removed superfluous rot_eq_tac from simplifier.ML HOL/simpdata.ML: renamed mk_meta_eq to meta_eq, re-renamed mk_meta_eq_simp to mk_meta_eq added Eps_eq to simpset
1998-07-30 wenzelm 1998-07-30 made SML/NJ happy;
1998-07-30 wenzelm 1998-07-30 functorized Clasimp module;
1998-07-02 paulson 1998-07-02 HACKED declaration of addsplits
1998-05-14 oheimb 1998-05-14 extended addsplits and delsplits to handle also split rules for assumptions extended const_of_split_thm, renamed it to split_thm_info
1998-04-04 wenzelm 1998-04-04 no open Simplifier;
1998-02-28 nipkow 1998-02-28 Splitters via named loopers.
1998-02-25 oheimb 1998-02-25 factored out common code of HOL/simpdata.ML and FOL/simpdata.ML concerning combination of classical reasoner and simplifier auto_tac into Provers/clasimp.ML explicitly introducing combined type clasimpset
1998-02-25 oheimb 1998-02-25 changed wrapper mechanism of classical reasoner
1997-12-24 paulson 1997-12-24 New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
1997-12-03 paulson 1997-12-03 Instantiated the one-point-rule quantifier simpprocs for FOL New file fologic.ML holds abstract syntax operations Also, miniscoping provided for intuitionistic logic
1997-11-28 paulson 1997-11-28 addsplits now in FOL, ZF too
1997-11-12 oheimb 1997-11-12 renamed split_prem_tac to split_asm_tac
1997-11-07 oheimb 1997-11-07 added split_prem_tac
1997-11-07 oheimb 1997-11-07 changed libraray function find to find_index_eq, currying it
1997-11-03 wenzelm 1997-11-03 adapted to new implicit simpset;
1997-10-17 paulson 1997-10-17 New simprules imp_disj1,2 and some comments
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-08-06 berghofe 1997-08-06 Moved functions from file "thy_data.ML".
1997-07-23 wenzelm 1997-07-23 standard congs;
1997-07-22 paulson 1997-07-22 Removal of the tactical STATE
1997-05-15 oheimb 1997-05-15 renamed addss to addSss, unsafe_addss to addss, extended auto_tac
1997-03-18 nipkow 1997-03-18 Added P&P&Q <-> P&Q and P|P|Q <-> P|Q
1997-03-05 paulson 1997-03-05 Eta-expanded declarations of addSIs2, etc., to avoid polymorphism errors
1997-02-15 oheimb 1997-02-15 added delcongs, Delcongs, unsafe_solver, safe_solver, FOL_basic_ss, safe_asm_more_full_simp_tac new addss (old version retained as unsafe_addss), new auto_tac (old version retained as unsafe_auto_tac), clasimpset with modification functions
1997-02-10 paulson 1997-02-10 Renamed structure Int (intuitionistic prover) to IntPr to prevent clash with Basis Library structure Int
1997-01-03 paulson 1997-01-03 Implicit simpsets and clasets for FOL and ZF
1996-10-09 paulson 1996-10-09 Added the de Morgan laws (incl quantifier versions) to basic simpset
1996-10-08 paulson 1996-10-08 Addition of one-point quantifier rewrite rules
1996-09-09 paulson 1996-09-09 Removal of (EX x. P) <-> P and (ALL x. P) <-> P from ex_simps and all_simps. as they are already in quant_simps.
1996-09-05 paulson 1996-09-05 Introduction of miniscoping for FOL
1996-08-19 paulson 1996-08-19 Added a lot of basic laws, from HOL/simpdata
1996-05-06 berghofe 1996-05-06 Added split_inside_tac.
1996-01-29 clasohm 1996-01-29 expanded tabs
1995-05-03 lcp 1995-05-03 Imported meta_eq_to_obj_eq from HOL for use with 'split'.
1995-03-30 lcp 1995-03-30 Defined addss to perform simplification in a claset. Precedence of addcongs is now 4 (to match that of other simplifier infixes)
1995-03-08 nipkow 1995-03-08 Enforced partial evaluation of mk_case_split_tac.
1994-12-14 lcp 1994-12-14 conj_commute,disj_commute: new
1994-11-30 clasohm 1994-11-30 added qed_goal for meta_iffD
1994-11-25 lcp 1994-11-25 added blank line
1994-06-17 lcp 1994-06-17 atomize: borrowed HOL version, which checks for both Trueprop and == as main connective (avoids using wildcard)
1994-05-24 nipkow 1994-05-24 Modified mk_meta_eq to leave meta-equlities on unchanged. Thus you may now add ==-thms to simpsets.
1994-05-13 lcp 1994-05-13 FOL/simpdata: added etac FalseE in setsolver call. Toby: "now that the simplifier can rewrite premises, it can generate the premise False."
1994-03-17 lcp 1994-03-17 FOL/simpdata: tidied FOL/simpdata/not_rews: moved the law "~(P|Q) <-> ~P & ~Q" from distrib_rews FOL/simpdata/cla_rews: added the law "~(P&Q) <-> ~P | ~Q"
1994-01-05 nipkow 1994-01-05 updated solver of FOL_ss. see change of HOL/simpdata.ML
1993-10-12 nipkow 1993-10-12 Added gen_all to simpdata.ML.
1993-09-16 nipkow 1993-09-16 defined local addcongs
1993-09-16 clasohm 1993-09-16 Initial revision