| Sun, 15 Apr 2007 14:32:07 +0200 |
wenzelm |
legacy_infer_term/prop -- including intern_term;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 17:35:52 +0200 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
file |
diff |
annotate
|
| Fri, 17 Feb 2006 01:46:38 +0100 |
huffman |
make maybe into a real type constructor; remove monad syntax
|
file |
diff |
annotate
|
| Wed, 30 Nov 2005 01:01:15 +0100 |
huffman |
reimplement Case expression pattern matching to support lazy patterns
|
file |
diff |
annotate
|
| Tue, 08 Nov 2005 02:19:11 +0100 |
huffman |
generate pattern combinators for new datatypes
|
file |
diff |
annotate
|
| Thu, 03 Nov 2005 03:06:02 +0100 |
huffman |
improve support for mutual recursion: now generates correct copy constant and induction theorem for mutually-recursive types; initial support for indirect recursion
|
file |
diff |
annotate
|
| Thu, 03 Nov 2005 02:19:48 +0100 |
huffman |
cleaned up; renamed library function mk_cRep_CFun to list_ccomb; replaced rep_TFree with dest_TFree; added functions spair, mk_stuple
|
file |
diff |
annotate
|
| Wed, 12 Oct 2005 03:02:18 +0200 |
huffman |
domain package generates compactness lemmas for new constructors
|
file |
diff |
annotate
|
| Mon, 10 Oct 2005 03:55:39 +0200 |
huffman |
replaced foldr' with foldr1
|
file |
diff |
annotate
|
| Mon, 10 Oct 2005 03:47:00 +0200 |
huffman |
cleaned up; renamed "Porder.op <<" to "Porder.<<"
|
file |
diff |
annotate
|
| Mon, 12 Sep 2005 18:20:32 +0200 |
haftmann |
introduced new-style AList operations
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2005 18:28:36 +0200 |
huffman |
use qualified names for all constants
|
file |
diff |
annotate
|
| Tue, 14 Jun 2005 23:44:37 +0200 |
huffman |
in domain declarations, selector names are now optional
|
file |
diff |
annotate
|
| Sat, 04 Jun 2005 00:24:33 +0200 |
huffman |
Domain package generates match functions for new datatypes, for use with the fixrec package
|
file |
diff |
annotate
|
| Thu, 31 Mar 2005 02:44:46 +0200 |
huffman |
fixed bug in prj' function
|
file |
diff |
annotate
|
| Fri, 11 Mar 2005 00:45:07 +0100 |
huffman |
fixed bug: domain package can now define three or more mutually recursive types simultaneously
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Thu, 22 Apr 2004 10:52:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 01:41:26 +0100 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Fri, 31 Aug 2001 16:26:55 +0200 |
berghofe |
Renamed functions % and %% to avoid clash with syntax for proof terms.
|
file |
diff |
annotate
|
| Wed, 29 Sep 1999 14:56:01 +0200 |
wenzelm |
Sign.of_sort;
|
file |
diff |
annotate
|
| Wed, 09 Sep 1998 16:21:08 +0200 |
oheimb |
renamed sswhen to sscase
|
file |
diff |
annotate
|
| Wed, 12 Aug 1998 14:56:56 +0200 |
oheimb |
minor correction: n must not be used as free variable
|
file |
diff |
annotate
|
| Wed, 12 Aug 1998 12:17:20 +0200 |
slotosch |
eliminated fabs,fapp.
|
file |
diff |
annotate
|
| Fri, 03 Apr 1998 13:30:49 +0200 |
oheimb |
repaired incompatibility with new SML version by eta-expansion
|
file |
diff |
annotate
|
| Tue, 24 Mar 1998 15:54:42 +0100 |
oheimb |
added cproj', and therefore extended prj
|
file |
diff |
annotate
|
| Mon, 09 Mar 1998 16:16:21 +0100 |
wenzelm |
Symbol.explode;
|
file |
diff |
annotate
|
| Fri, 07 Nov 1997 18:02:15 +0100 |
oheimb |
changed libraray function find to find_index_eq, currying it
|
file |
diff |
annotate
|
| Tue, 04 Nov 1997 14:40:29 +0100 |
oheimb |
* removed "axioms" and "generated by" section
|
file |
diff |
annotate
|
| Thu, 30 Oct 1997 14:19:01 +0100 |
oheimb |
domain package:
|
file |
diff |
annotate
|
| Mon, 27 Oct 1997 11:34:33 +0100 |
oheimb |
adapted domain and ax_ops package for name spaces
|
file |
diff |
annotate
|
| Fri, 06 Jun 1997 16:02:13 +0200 |
oheimb |
improved function 'nonreserved'
|
file |
diff |
annotate
|
| Tue, 13 May 1997 15:02:19 +0200 |
oheimb |
corrected problem with type abbreviations in pcpo_type
|
file |
diff |
annotate
|
| Tue, 04 Mar 1997 10:58:29 +0100 |
paulson |
Renamed constant "not" to "Not"
|
file |
diff |
annotate
|
| Wed, 18 Dec 1996 15:19:42 +0100 |
oheimb |
The previous log message was wrong. The correct one is:
|
file |
diff |
annotate
|
| Wed, 18 Dec 1996 15:16:13 +0100 |
oheimb |
removed Holcfb.thy and Holcfb.ML, moving classical3 to HOL.ML as classical2
|
file |
diff |
annotate
|
| Fri, 29 Nov 1996 12:16:57 +0100 |
oheimb |
modified file headers
|
file |
diff |
annotate
|
| Wed, 27 Nov 1996 10:40:45 +0100 |
paulson |
Eta-expanded some declarations that are illegal under value polymorphism
|
file |
diff |
annotate
|
| Thu, 27 Jun 1996 15:24:17 +0200 |
oheimb |
re-added when_funs to library.ML
|
file |
diff |
annotate
|
| Wed, 26 Jun 1996 17:37:34 +0200 |
oheimb |
when_funs removed
|
file |
diff |
annotate
|
| Fri, 21 Jun 1996 11:57:00 +0200 |
oheimb |
minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)
|
file |
diff |
annotate
|
| Wed, 03 Apr 1996 19:27:14 +0200 |
oheimb |
Updated: 01-Mar-96 when functional strictified, copy_def based on when_def
|
file |
diff |
annotate
|
| Tue, 30 Jan 1996 13:42:57 +0100 |
clasohm |
expanded tabs
|
file |
diff |
annotate
|
| Fri, 06 Oct 1995 17:25:24 +0100 |
regensbu |
added 8bit pragmas
|
file |
diff |
annotate
|