| Thu, 13 Apr 2000 15:01:50 +0200 |
nipkow |
Times -> <*>
|
file |
diff |
annotate
|
| 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
|