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.