src/HOL/simpdata.ML
1996-12-18 oheimb 1996-12-18 factored out HOL_base_ss and val HOL_min_ss, added HOL_safe_min_ss
1996-11-27 oheimb 1996-11-27 moved split_tac
1996-11-27 oheimb 1996-11-27 moved if_cancel to the right place
1996-11-27 oheimb 1996-11-27 added if_cancel later to simpset
1996-11-26 oheimb 1996-11-26 if_cancel added to HOL_ss
1996-10-28 nipkow 1996-10-28 Renamed and shuffled a few thms.
1996-10-25 nipkow 1996-10-25 Added (? x. t=x) = True
1996-10-15 oheimb 1996-10-15 corrected `correction` of o_assoc (of version 1.14), (this change has actually been done in the previous commit 1.25)
1996-10-15 oheimb 1996-10-15 bound o_apply theorem to thy
1996-10-10 paulson 1996-10-10 Addition of de Morgan laws
1996-10-07 paulson 1996-10-07 New one-point rules for quantifiers
1996-09-26 paulson 1996-09-26 Ran expandshort; used stac instead of ssubst
1996-09-26 paulson 1996-09-26 Ran expandshort
1996-09-24 paulson 1996-09-24 Fixed spelling error in comment
1996-09-12 paulson 1996-09-12 Installed AddIffs, and some code from HOL.ML
1996-09-10 paulson 1996-09-10 Beefed-up auto-tactic: now repeatedly simplifies if needed
1996-09-05 paulson 1996-09-05 Added miniscoping to the simplifier: quantifiers are now pushed in
1996-08-19 paulson 1996-08-19 Installation of auto_tac; re-organization
1996-07-29 paulson 1996-07-29 Added two new distributive laws
1996-07-17 pusch 1996-07-17 Corrected o_assoc lemma
1996-06-21 berghofe 1996-06-21 Added function Addss.
1996-05-22 nipkow 1996-05-22 Added ex_imp
1996-05-06 berghofe 1996-05-06 Added split_inside_tac.
1996-04-17 oheimb 1996-04-17 *** empty log message ***
1996-04-11 nipkow 1996-04-11 Added a number of lemmas
1996-03-06 nipkow 1996-03-06 Added 'section' commands
1996-02-09 nipkow 1996-02-09 Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
1996-01-30 clasohm 1996-01-30 expanded tabs
1995-10-04 clasohm 1995-10-04 added local simpsets; removed IOA from 'make test'
1995-03-31 lcp 1995-03-31 Defined addss to perform simplification in a claset. Precedence of addcongs is now 4 (to match that of other simplifier infixes)
1995-03-20 clasohm 1995-03-20 changed syntax of "if"
1995-03-08 nipkow 1995-03-08 Enforced partial evaluation of mk_case_split_tac
1995-03-03 clasohm 1995-03-03 new version of HOL with curried function application