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