1999-08-25 wenzelm 1999-08-25 proper bootstrap of HOL theory and packages;
1999-08-02 wenzelm 1999-08-02 tuned;
1999-07-15 paulson 1999-07-15 qed_goal -> Goal
1998-11-18 wenzelm 1998-11-18 blast: cla_method';
1998-02-25 oheimb 1998-02-25 renamed rep_claset to rep_cs
1998-01-08 oheimb 1998-01-08 added select_equality to the implicit claset
1997-12-23 paulson 1997-12-23 Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
1997-11-26 paulson 1997-11-26 The change from iffE to iffCE means fewer case splits in most cases. Very few proofs are affected, almost none adversely
1997-11-20 paulson 1997-11-20 Renamed "overload" to "overloaded" for sml/nj compatibility
1997-11-12 oheimb 1997-11-12 added thin_refl to hyp_subst_tac
1997-11-12 oheimb 1997-11-12 restored last version
1997-11-12 oheimb 1997-11-12 simpdata.ML: renamed split_prem_tac to split_asm_tac, added split_if_asm cladata.ML: unintentinally committed
1997-11-06 paulson 1997-11-06 hyp_subst_tac checks if the equality has type variables and uses a suitable method if so. Affects the dest_eq function
1997-11-03 wenzelm 1997-11-03 adapted to new implicit claset;
1997-11-01 paulson 1997-11-01 New Blast_tac (and minor tidying...)
1997-10-10 wenzelm 1997-10-10 fixed dots;
1997-08-06 berghofe 1997-08-06 Moved some functions which used to be part of thy_data.ML
1997-04-21 paulson 1997-04-21 New elimination rule for "unique existence"
1997-04-03 paulson 1997-04-03 Declares overloading for if-and-only-if
1997-04-02 paulson 1997-04-02 Installation of blast_tac
1996-09-12 paulson 1996-09-12 Tidied many proofs, using AddIffs to let equivalences take the place of separate Intr and Elim rules. Also deleted most named clasets.