| Fri, 11 Nov 2005 00:09:37 +0100 | huffman | add header | file | diff | annotate |
| Fri, 21 Oct 2005 18:14:34 +0200 | wenzelm | Goal.prove; | file | diff | annotate |
| Mon, 17 Oct 2005 23:10:15 +0200 | wenzelm | Simplifier.inherit_context instead of Simplifier.inherit_bounds; | file | diff | annotate |
| Thu, 22 Sep 2005 23:56:15 +0200 | nipkow | renamed rules to iprover | file | diff | annotate |
| Tue, 16 Aug 2005 15:36:28 +0200 | paulson | classical rules must have names for ATP integration | file | diff | annotate |
| Mon, 01 Aug 2005 19:20:26 +0200 | wenzelm | simprocs: Simplifier.inherit_bounds; | file | diff | annotate |
| Thu, 07 Jul 2005 12:39:17 +0200 | nipkow | linear arithmetic now takes "&" in assumptions apart. | file | diff | annotate |
| Sun, 10 Apr 2005 17:19:03 +0200 | nipkow | _(_|_) is now override_on | file | diff | annotate |
| Sun, 13 Feb 2005 17:15:14 +0100 | skalberg | Deleted Library.option type. | file | diff | annotate |
| Wed, 09 Feb 2005 18:32:28 +0100 | paulson | new foldSet proofs | file | diff | annotate |
| Fri, 14 Jan 2005 12:00:27 +0100 | nipkow | made diff_less a simp rule | file | diff | annotate |
| Sun, 21 Nov 2004 15:44:20 +0100 | nipkow | added lemmas | file | diff | annotate |
| Wed, 18 Aug 2004 11:09:40 +0200 | nipkow | import -> imports | file | diff | annotate |
| Mon, 16 Aug 2004 14:22:27 +0200 | nipkow | New theory header syntax. | file | diff | annotate |
| Wed, 04 Aug 2004 19:11:02 +0200 | nipkow | added some inj_on thms | file | diff | annotate |
| Wed, 14 Apr 2004 14:13:05 +0200 | kleing | use more symbols in HTML output | file | diff | annotate |
| 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 |