src/HOL/cladata.ML
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2001-12-04 wenzelm 2001-12-04 hyp_subst_tac';
2001-10-14 wenzelm 2001-10-14 improved atomize setup;
2001-07-25 paulson 2001-07-25 partial restructuring to reduce dependence on Axiom of Choice
2001-07-22 wenzelm 2001-07-22 the_equality [intro];
2001-01-16 wenzelm 2001-01-16 tuned atomize;
2000-11-10 wenzelm 2000-11-10 val atomize = thms "atomize'";
2000-11-03 wenzelm 2000-11-03 "atomize" for classical tactics;
2000-10-17 paulson 2000-10-17 renaming of contrapos rules
2000-10-12 paulson 2000-10-12 renamed ?Pa to ?Q in swap
2000-09-15 paulson 2000-09-15 renamed (most of...) the select rules
2000-09-05 wenzelm 2000-09-05 tuned;
2000-08-04 wenzelm 2000-08-04 val rev_eq_reflection = def_imp_eq;
2000-07-30 wenzelm 2000-07-30 updated ObtainFun;
2000-06-28 paulson 2000-06-28 declaring and using cla_make_elim
2000-01-05 wenzelm 2000-01-05 ObtainFun;
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.