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