| Wed, 26 Sep 2007 20:27:55 +0200 |
haftmann |
moved Finite_Set before Datatype
|
file |
diff |
annotate
|
| Wed, 06 Jun 2007 23:06:29 +0200 |
huffman |
use new-style class for sq_ord; rename op << to sq_le
|
file |
diff |
annotate
|
| Sun, 26 Nov 2006 18:07:16 +0100 |
wenzelm |
updated (binder) syntax/notation;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2006 23:42:43 +0200 |
wenzelm |
fixed translations: CONST;
|
file |
diff |
annotate
|
| Fri, 12 May 2006 04:20:02 +0200 |
huffman |
add new finite chain theorems
|
file |
diff |
annotate
|
| Sun, 19 Feb 2006 02:11:27 +0100 |
huffman |
use minimal imports
|
file |
diff |
annotate
|
| Wed, 11 Jan 2006 03:10:04 +0100 |
huffman |
add transitivity rules
|
file |
diff |
annotate
|
| Fri, 04 Nov 2005 22:27:40 +0100 |
huffman |
cleaned up
|
file |
diff |
annotate
|
| Thu, 03 Nov 2005 00:16:09 +0100 |
huffman |
cleaned up; chain_const and thelub_const are simp rules
|
file |
diff |
annotate
|
| Mon, 10 Oct 2005 03:47:00 +0200 |
huffman |
cleaned up; renamed "Porder.op <<" to "Porder.<<"
|
file |
diff |
annotate
|
| Tue, 13 Sep 2005 23:30:01 +0200 |
huffman |
add theorem chain_const
|
file |
diff |
annotate
|
| Wed, 08 Jun 2005 00:59:46 +0200 |
huffman |
added theorems is_ub_range_shift and is_lub_range_shift
|
file |
diff |
annotate
|
| Fri, 27 May 2005 00:15:24 +0200 |
huffman |
added lemma thelub_const
|
file |
diff |
annotate
|
| Wed, 25 May 2005 09:44:34 +0200 |
wenzelm |
removed LICENCE note -- everything is subject to Isabelle licence as
|
file |
diff |
annotate
|
| Fri, 06 May 2005 03:47:44 +0200 |
huffman |
Replaced all unnecessary uses of SOME with THE or LEAST
|
file |
diff |
annotate
|
| Thu, 10 Mar 2005 20:22:45 +0100 |
huffman |
fixed filename in header
|
file |
diff |
annotate
|
| Mon, 07 Mar 2005 23:54:01 +0100 |
huffman |
added subsections and text for document generation
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 23:23:47 +0100 |
huffman |
fix headers
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 23:12:36 +0100 |
huffman |
converted to new-style theories, and combined numbered files
|
file |
diff |
annotate
|
| Wed, 02 Mar 2005 22:30:00 +0100 |
huffman |
converted to new-style theory
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Sat, 01 Dec 2001 18:52:32 +0100 |
wenzelm |
renamed class "term" to "type" (actually "HOL.type");
|
file |
diff |
annotate
|
| Fri, 09 Nov 2001 00:09:47 +0100 |
wenzelm |
eliminated old "symbols" syntax, use "xsymbols" instead;
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 01:41:26 +0100 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Thu, 31 May 2001 16:52:32 +0200 |
oheimb |
corrected ML names of definitions
|
file |
diff |
annotate
|
| Tue, 10 Mar 1998 18:33:13 +0100 |
oheimb |
renamed is_chain to chain, is_tord to tord, replaced chain_finite by chfin
|
file |
diff |
annotate
|
| Fri, 10 Oct 1997 19:02:28 +0200 |
wenzelm |
fixed dots;
|
file |
diff |
annotate
|
| Mon, 17 Feb 1997 10:57:11 +0100 |
slotosch |
Changes of HOLCF from Oscar Slotosch:
|
file |
diff |
annotate
|
| Fri, 13 Dec 1996 18:45:58 +0100 |
oheimb |
adaptions for symbol font
|
file |
diff |
annotate
|
| Mon, 02 Dec 1996 12:37:15 +0100 |
oheimb |
removed 8bit sections
|
file |
diff |
annotate
|
| Fri, 29 Nov 1996 12:22:22 +0100 |
oheimb |
*** empty log message ***
|
file |
diff |
annotate
|
| Tue, 06 Feb 1996 12:42:31 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Fri, 06 Oct 1995 17:25:24 +0100 |
regensbu |
added 8bit pragmas
|
file |
diff |
annotate
|
| Thu, 29 Jun 1995 16:28:40 +0200 |
regensbu |
The curried version of HOLCF is now just called HOLCF. The old
|
file |
diff |
annotate
|
| Thu, 24 Mar 1994 13:36:34 +0100 |
nipkow |
Franz fragen
|
file |
diff |
annotate
|
| Wed, 19 Jan 1994 17:35:01 +0100 |
nipkow |
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
|
file |
diff |
annotate
|