| Wed, 01 Mar 2000 15:00:21 +0100 |
paulson |
expandshort
|
file |
diff |
annotate
|
| Fri, 18 Feb 2000 20:25:29 +0100 |
oheimb |
added split_eta_SetCompr, SetCompr_Sigma_eq
|
file |
diff |
annotate
|
| Fri, 18 Feb 2000 15:35:29 +0100 |
paulson |
new distributive laws
|
file |
diff |
annotate
|
| Fri, 28 Jan 2000 14:08:54 +0100 |
oheimb |
added splitE', also to claset
|
file |
diff |
annotate
|
| Wed, 05 Jan 2000 11:56:04 +0100 |
wenzelm |
replaced HOLogic.termTVar by HOLogic.termT;
|
file |
diff |
annotate
|
| Wed, 27 Oct 1999 19:32:19 +0200 |
oheimb |
added various little lemmas
|
file |
diff |
annotate
|
| Mon, 06 Sep 1999 18:18:49 +0200 |
oheimb |
added theorems fst_eqD and snd_eqD, added split_beta_proc, new split_eta_proc
|
file |
diff |
annotate
|
| Wed, 25 Aug 1999 10:53:19 +0200 |
paulson |
split_paired_Eps and lemmas
|
file |
diff |
annotate
|
| Mon, 19 Jul 1999 15:24:35 +0200 |
paulson |
getting rid of qed_goal
|
file |
diff |
annotate
|
| Thu, 15 Jul 1999 10:27:54 +0200 |
paulson |
qed_goal -> Goal
|
file |
diff |
annotate
|
| Thu, 17 Jun 1999 10:33:33 +0200 |
paulson |
renamed UNION_... to UN_... (to fit the convention)
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 16:53:46 +0100 |
wenzelm |
Theory.sign_of;
|
file |
diff |
annotate
|
| Fri, 04 Dec 1998 10:44:02 +0100 |
paulson |
new (and generalized) theorems about Sigma/Times
|
file |
diff |
annotate
|
| Mon, 09 Nov 1998 10:59:47 +0100 |
paulson |
new TIMES/Sigma rules
|
file |
diff |
annotate
|
| Mon, 02 Nov 1998 15:31:29 +0100 |
paulson |
Domain r, Range r replace fst``r, snd``r
|
file |
diff |
annotate
|
| Fri, 23 Oct 1998 22:36:49 +0200 |
berghofe |
Added theorem unit_induct (for rep_datatype).
|
file |
diff |
annotate
|
| Wed, 21 Oct 1998 17:40:35 +0200 |
berghofe |
Added theorem prod_induct (needed for rep_datatype).
|
file |
diff |
annotate
|
| Tue, 20 Oct 1998 16:39:14 +0200 |
wenzelm |
split_paired_all.ML;
|
file |
diff |
annotate
|
| Thu, 24 Sep 1998 17:17:14 +0200 |
oheimb |
renamed mk_meta_eq to mk_eq
|
file |
diff |
annotate
|
| Mon, 24 Aug 1998 14:02:40 +0200 |
oheimb |
debugged split_eta_proc
|
file |
diff |
annotate
|
| Thu, 13 Aug 1998 18:14:26 +0200 |
paulson |
even more tidying of Goal commands
|
file |
diff |
annotate
|
| 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
|