| 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
|
| Thu, 03 Apr 1997 09:46:42 +0200 |
nipkow |
Removed (Unit) in Prod.
|
file |
diff |
annotate
|
| Wed, 02 Apr 1997 11:19:46 +0200 |
paulson |
Reorganization of how classical rules are installed
|
file |
diff |
annotate
|
| Sat, 15 Feb 1997 17:52:31 +0100 |
oheimb |
reflecting my recent changes of the simplifier and classical reasoner
|
file |
diff |
annotate
|
| Thu, 10 Oct 1996 12:00:23 +0200 |
paulson |
Deleted obsolete clasets
|
file |
diff |
annotate
|
| Thu, 26 Sep 1996 12:47:47 +0200 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Tue, 21 May 1996 13:39:31 +0200 |
berghofe |
Replaced fast_tac by Fast_tac (which uses default claset)
|
file |
diff |
annotate
|
| Fri, 17 May 1996 12:23:44 +0200 |
nipkow |
Moved split_rule et al from ind_syntax.ML to Prod.ML.
|
file |
diff |
annotate
|
| Tue, 07 May 1996 18:14:39 +0200 |
paulson |
Now split_all_tac works for i>1 !
|
file |
diff |
annotate
|
| Thu, 11 Apr 1996 08:30:25 +0200 |
nipkow |
Added a number of lemmas
|
file |
diff |
annotate
|
| Thu, 04 Apr 1996 11:45:01 +0200 |
paulson |
Using new "Times" infix
|
file |
diff |
annotate
|
| Wed, 27 Mar 1996 18:45:17 +0100 |
paulson |
Library changes for mutilated checkerboard
|
file |
diff |
annotate
|
| Wed, 06 Mar 1996 12:52:11 +0100 |
paulson |
Ran expandshort
|
file |
diff |
annotate
|
| Mon, 19 Feb 1996 18:04:41 +0100 |
nipkow |
Introduced normalize_thm into HOL.ML
|
file |
diff |
annotate
|
| Fri, 09 Feb 1996 13:41:18 +0100 |
nipkow |
Added qed_spec_mp to avoid renaming of bound vars in 'th RS spec'
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 15:24:36 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Fri, 26 Jan 1996 20:25:39 +0100 |
nipkow |
Streamlined defs in Relation and added new intro/elim rules to do with
|
file |
diff |
annotate
|
| Wed, 25 Oct 1995 09:48:29 +0100 |
nipkow |
Added various thms and tactics.
|
file |
diff |
annotate
|
| Wed, 04 Oct 1995 13:10:03 +0100 |
clasohm |
added local simpsets; removed IOA from 'make test'
|
file |
diff |
annotate
|
| Fri, 24 Mar 1995 12:30:35 +0100 |
clasohm |
changed syntax of tuples from <..., ...> to (..., ...)
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 12:02:25 +0100 |
clasohm |
new version of HOL with curried function application
|
file |
diff |
annotate
|