src/FOL/simpdata.ML
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