src/HOL/cladata.ML
Tue, 04 Dec 2001 02:01:31 +0100 wenzelm hyp_subst_tac';
Sun, 14 Oct 2001 20:02:59 +0200 wenzelm improved atomize setup;
Wed, 25 Jul 2001 13:13:01 +0200 paulson partial restructuring to reduce dependence on Axiom of Choice
Sun, 22 Jul 2001 21:31:00 +0200 wenzelm the_equality [intro];
Tue, 16 Jan 2001 00:28:50 +0100 wenzelm tuned atomize;
Fri, 10 Nov 2000 19:00:22 +0100 wenzelm val atomize = thms "atomize'";
Fri, 03 Nov 2000 21:31:11 +0100 wenzelm "atomize" for classical tactics;
Tue, 17 Oct 2000 10:21:12 +0200 paulson renaming of contrapos rules
Thu, 12 Oct 2000 12:16:22 +0200 paulson renamed ?Pa to ?Q in swap
Fri, 15 Sep 2000 12:39:57 +0200 paulson renamed (most of...) the select rules
Tue, 05 Sep 2000 18:43:22 +0200 wenzelm tuned;
Fri, 04 Aug 2000 22:57:37 +0200 wenzelm val rev_eq_reflection = def_imp_eq;
Sun, 30 Jul 2000 13:01:50 +0200 wenzelm updated ObtainFun;
Wed, 28 Jun 2000 10:37:52 +0200 paulson declaring and using cla_make_elim
Wed, 05 Jan 2000 11:50:55 +0100 wenzelm ObtainFun;
Wed, 25 Aug 1999 20:49:02 +0200 wenzelm proper bootstrap of HOL theory and packages;
Mon, 02 Aug 1999 17:58:46 +0200 wenzelm tuned;
Thu, 15 Jul 1999 10:27:54 +0200 paulson qed_goal -> Goal
Wed, 18 Nov 1998 11:03:49 +0100 wenzelm blast: cla_method';
Wed, 25 Feb 1998 20:29:58 +0100 oheimb renamed rep_claset to rep_cs
Thu, 08 Jan 1998 18:09:07 +0100 oheimb added select_equality to the implicit claset
Tue, 23 Dec 1997 11:39:03 +0100 paulson Better equality handling in Blast_tac, usingd a new variant of hyp_subst_tac
Wed, 26 Nov 1997 17:31:02 +0100 paulson The change from iffE to iffCE means fewer case splits in most cases. Very few
Thu, 20 Nov 1997 10:54:04 +0100 paulson Renamed "overload" to "overloaded" for sml/nj compatibility
Wed, 12 Nov 1997 18:58:50 +0100 oheimb added thin_refl to hyp_subst_tac
Wed, 12 Nov 1997 12:34:43 +0100 oheimb restored last version
Wed, 12 Nov 1997 12:30:15 +0100 oheimb simpdata.ML: renamed split_prem_tac to split_asm_tac, added split_if_asm
Thu, 06 Nov 1997 10:29:37 +0100 paulson hyp_subst_tac checks if the equality has type variables and uses a suitable
Mon, 03 Nov 1997 12:09:20 +0100 wenzelm adapted to new implicit claset;
Sat, 01 Nov 1997 12:59:06 +0100 paulson New Blast_tac (and minor tidying...)
Fri, 10 Oct 1997 19:02:28 +0200 wenzelm fixed dots;
Wed, 06 Aug 1997 01:13:46 +0200 berghofe Moved some functions which used to be part of thy_data.ML
Mon, 21 Apr 1997 12:16:29 +0200 paulson New elimination rule for "unique existence"
Thu, 03 Apr 1997 10:30:23 +0200 paulson Declares overloading for if-and-only-if
Wed, 02 Apr 1997 11:30:03 +0200 paulson Installation of blast_tac
Thu, 12 Sep 1996 10:40:05 +0200 paulson Tidied many proofs, using AddIffs to let equivalences take
less more (0) tip