Thu, 03 Nov 2005 02:37:09 +0100 |
huffman |
reimplement copy_def to use data constructor constants
|
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
|
Thu, 03 Nov 2005 00:43:50 +0100 |
huffman |
changed iterate to a continuous type
|
file |
diff |
annotate
|
Mon, 10 Oct 2005 03:55:39 +0200 |
huffman |
replaced foldr' with foldr1
|
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
|
Thu, 09 Jun 2005 12:03:19 +0200 |
wenzelm |
add_axioms_infer -- avoids use of stale theory;
|
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
|
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
|
Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
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
|
Mon, 13 Mar 2000 13:28:31 +0100 |
wenzelm |
adapted to new PureThy.add_thms etc.;
|
file |
diff |
annotate
|
Tue, 12 Jan 1999 13:54:51 +0100 |
wenzelm |
eliminated tthm type and Attribute structure;
|
file |
diff |
annotate
|
Wed, 12 Aug 1998 12:17:20 +0200 |
slotosch |
eliminated fabs,fapp.
|
file |
diff |
annotate
|
Wed, 29 Apr 1998 11:36:53 +0200 |
wenzelm |
adapted to new PureThy.add_axioms_i;
|
file |
diff |
annotate
|
Tue, 24 Mar 1998 15:57:18 +0100 |
oheimb |
added cproj', and therefore extended prj
|
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
|
Thu, 02 Oct 1997 22:54:00 +0200 |
wenzelm |
fully qualified names: Theory.add_XXX;
|
file |
diff |
annotate
|
Mon, 17 Feb 1997 11:01:10 +0100 |
slotosch |
using types one = unit lift and translations causes troubles between
|
file |
diff |
annotate
|
Thu, 19 Dec 1996 17:02:27 +0100 |
oheimb |
corrected headers
|
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
|