| Wed, 12 Aug 1998 16:20:49 +0200 |
oheimb |
renamed mk_meta_eq to meta_eq
|
file |
diff |
annotate
|
| Wed, 12 Aug 1998 15:18:34 +0200 |
oheimb |
replaced split_etas by split_eta_proc
|
file |
diff |
annotate
|
| Thu, 06 Aug 1998 15:48:13 +0200 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
| Wed, 15 Jul 1998 10:58:44 +0200 |
nipkow |
Minor tidying up.
|
file |
diff |
annotate
|
| Wed, 15 Jul 1998 10:15:13 +0200 |
paulson |
Removal of leading "\!\!..." from most Goal commands
|
file |
diff |
annotate
|
| Sun, 12 Jul 1998 11:49:17 +0200 |
wenzelm |
isatool expandshort;
|
file |
diff |
annotate
|
| Tue, 30 Jun 1998 20:41:41 +0200 |
berghofe |
Moved most of the Prod_Syntax - stuff to HOLogic.
|
file |
diff |
annotate
|
| Fri, 26 Jun 1998 15:10:40 +0200 |
paulson |
New rewrite unit_abs_eta_conv to compensate for unit_eq_proc
|
file |
diff |
annotate
|
| Thu, 25 Jun 1998 15:34:17 +0200 |
wenzelm |
added unit_eq simplification procedure;
|
file |
diff |
annotate
|
| Mon, 22 Jun 1998 17:26:46 +0200 |
wenzelm |
isatool fixgoal;
|
file |
diff |
annotate
|
| Tue, 02 Jun 1998 15:07:25 +0200 |
oheimb |
added split_etas
|
file |
diff |
annotate
|
| Mon, 27 Apr 1998 16:45:11 +0200 |
nipkow |
Added a few lemmas.
|
file |
diff |
annotate
|
| Fri, 24 Apr 1998 16:18:39 +0200 |
oheimb |
improved split_all_tac significantly
|
file |
diff |
annotate
|
| Tue, 21 Apr 1998 17:25:19 +0200 |
oheimb |
improved pair_tac to call prune_params_tac afterwards
|
file |
diff |
annotate
|
| Tue, 07 Apr 1998 13:43:07 +0200 |
oheimb |
made split_all_tac as safe wrapper more defensive:
|
file |
diff |
annotate
|
| Thu, 02 Apr 1998 17:19:02 +0200 |
oheimb |
split_all_tac now fails if there is nothing to split
|
file |
diff |
annotate
|
| Wed, 25 Feb 1998 15:48:04 +0100 |
oheimb |
added split_all_tac to claset()
|
file |
diff |
annotate
|
| Thu, 08 Jan 1998 18:08:43 +0100 |
oheimb |
added select_equality to the implicit claset
|
file |
diff |
annotate
|
| Thu, 08 Jan 1998 11:21:45 +0100 |
paulson |
Tidied by adding more default simprules
|
file |
diff |
annotate
|
| Thu, 18 Dec 1997 12:50:58 +0100 |
oheimb |
added expand_split_asm
|
file |
diff |
annotate
|
| Tue, 16 Dec 1997 17:58:03 +0100 |
wenzelm |
expandshort;
|
file |
diff |
annotate
|
| Mon, 10 Nov 1997 14:57:31 +0100 |
oheimb |
replaced 8bit characters
|
file |
diff |
annotate
|
| Tue, 04 Nov 1997 20:49:45 +0100 |
oheimb |
added several theorems
|
file |
diff |
annotate
|
| Mon, 03 Nov 1997 12:13:18 +0100 |
wenzelm |
isatool fixclasimp;
|
file |
diff |
annotate
|
| Fri, 17 Oct 1997 15:25:12 +0200 |
nipkow |
setloop split_tac -> addsplits
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 19:02:28 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Wed, 23 Jul 1997 17:43:42 +0200 |
nipkow |
Prod.ML: Added split_paired_EX and lots of comments about failed attempts to
|
file |
diff |
annotate
|
| Fri, 06 Jun 1997 19:30:06 +0200 |
nipkow |
Added
|
file |
diff |
annotate
|
| Fri, 11 Apr 1997 15:21:36 +0200 |
paulson |
Yet more fast_tac->blast_tac, and other tidying
|
file |
diff |
annotate
|
| Thu, 03 Apr 1997 19:29:53 +0200 |
nipkow |
Now: unit = {True}
|
file |
diff |
annotate
|