| Mon, 14 Apr 2003 18:52:13 +0200 |
nipkow |
Added thms
|
file |
diff |
annotate
|
| Thu, 10 Oct 2002 14:21:20 +0200 |
berghofe |
- Added range_ex1_eq
|
file |
diff |
annotate
|
| Thu, 26 Sep 2002 10:51:29 +0200 |
paulson |
Converted Fun to Isar style.
|
file |
diff |
annotate
|
| Tue, 11 Dec 2001 13:43:00 +0100 |
wenzelm |
oops;
|
file |
diff |
annotate
|
| Mon, 10 Dec 2001 20:59:43 +0100 |
wenzelm |
bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";
|
file |
diff |
annotate
|
| Sat, 01 Dec 2001 18:52:32 +0100 |
wenzelm |
renamed class "term" to "type" (actually "HOL.type");
|
file |
diff |
annotate
|
| Wed, 21 Nov 2001 00:33:40 +0100 |
wenzelm |
got rid of theory Inverse_Image;
|
file |
diff |
annotate
|
| Fri, 09 Nov 2001 00:09:47 +0100 |
wenzelm |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
file |
diff |
annotate
|
| Thu, 27 Sep 2001 22:28:16 +0200 |
wenzelm |
eliminated theories "equalities" and "mono" (made part of "Typedef",
|
file |
diff |
annotate
|
| Wed, 25 Jul 2001 13:13:01 +0200 |
paulson |
partial restructuring to reduce dependence on Axiom of Choice
|
file |
diff |
annotate
|
| Wed, 14 Feb 2001 20:45:35 +0100 |
oheimb |
removed whitespace
|
file |
diff |
annotate
|
| Mon, 08 Jan 2001 12:27:36 +0100 |
nipkow |
Removed Applyall
|
file |
diff |
annotate
|
| Thu, 12 Oct 2000 18:38:23 +0200 |
nipkow |
*** empty log message ***
|
file |
diff |
annotate
|
| Sun, 16 Jul 2000 20:48:35 +0200 |
wenzelm |
syntax (symbols) "op o" moved from HOL to Fun;
|
file |
diff |
annotate
|
| Fri, 14 Jul 2000 16:27:45 +0200 |
oheimb |
added hint on fun_sum
|
file |
diff |
annotate
|
| Thu, 13 Jul 2000 23:08:42 +0200 |
wenzelm |
fixed compose decl;
|
file |
diff |
annotate
|
| Sun, 25 Jun 2000 23:58:27 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 24 May 2000 18:48:03 +0200 |
paulson |
we must not require SetInterval this early
|
file |
diff |
annotate
|
| Tue, 23 May 2000 07:32:24 +0200 |
nipkow |
Added SetInterval
|
file |
diff |
annotate
|
| Fri, 18 Feb 2000 20:24:16 +0100 |
oheimb |
changed precedence of function update
|
file |
diff |
annotate
|
| Fri, 27 Aug 1999 15:41:11 +0200 |
paulson |
the bij predicate (at last)
|
file |
diff |
annotate
|
| Wed, 03 Feb 1999 13:26:07 +0100 |
paulson |
inj is now a translation of inj_on
|
file |
diff |
annotate
|
| Fri, 13 Nov 1998 13:26:16 +0100 |
paulson |
the function space operator
|
file |
diff |
annotate
|
| Fri, 02 Oct 1998 14:28:39 +0200 |
nipkow |
id <-> Id
|
file |
diff |
annotate
|
| Wed, 12 Aug 1998 16:23:25 +0200 |
oheimb |
cleanup for Fun.thy:
|
file |
diff |
annotate
|
| Mon, 27 Apr 1998 16:45:11 +0200 |
nipkow |
Added a few lemmas.
|
file |
diff |
annotate
|
| Tue, 24 Feb 1998 11:35:33 +0100 |
paulson |
New theory of the inverse image of a function
|
file |
diff |
annotate
|
| Sat, 01 Nov 1997 12:59:06 +0100 |
paulson |
New Blast_tac (and minor tidying...)
|
file |
diff |
annotate
|
| Fri, 04 Apr 1997 16:33:28 +0200 |
nipkow |
moved inj and surj from Set to Fun and Inv -> inv.
|
file |
diff |
annotate
|
| Mon, 05 Feb 1996 21:27:16 +0100 |
clasohm |
expanded tabs; renamed subtype to typedef;
|
file |
diff |
annotate
|
| Fri, 03 Mar 1995 12:02:25 +0100 |
clasohm |
new version of HOL with curried function application
|
file |
diff |
annotate
|