| Sat, 14 Apr 2007 17:35:52 +0200 |
wenzelm |
cleaned/simplified Sign.read_typ, Thm.read_cterm etc.;
|
file |
diff |
annotate
|
| Sun, 30 Apr 2006 22:50:03 +0200 |
wenzelm |
AxClass.axiomatize_arity_i;
|
file |
diff |
annotate
|
| Tue, 07 Feb 2006 19:56:45 +0100 |
wenzelm |
renamed gen_duplicates to duplicates;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 11:01:28 +0100 |
haftmann |
subsituted gen_duplicates / has_duplicates for duplicates whenever appropriate
|
file |
diff |
annotate
|
| Fri, 09 Dec 2005 09:06:45 +0100 |
haftmann |
oriented result pairs in PureThy
|
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
|
| Mon, 12 Sep 2005 18:20:32 +0200 |
haftmann |
introduced new-style AList operations
|
file |
diff |
annotate
|
| Tue, 16 Aug 2005 13:42:26 +0200 |
wenzelm |
OuterKeyword;
|
file |
diff |
annotate
|
| Tue, 14 Jun 2005 23:44:37 +0200 |
huffman |
in domain declarations, selector names are now optional
|
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, 11 Mar 2005 00:43:52 +0100 |
huffman |
domain package now permits indirect recursion with these type constructors: *, ->, ++, **, u
|
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
|
| Tue, 07 Sep 2004 15:59:16 +0200 |
oheimb |
added check against indirect recursion
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Fri, 11 Jul 2003 13:54:32 +0200 |
oheimb |
re-introduced sort constraints on LHS
|
file |
diff |
annotate
|
| Tue, 12 Feb 2002 20:28:27 +0100 |
wenzelm |
got rid of explicit marginal comments (now stripped earlier from input);
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 18:42:00 +0100 |
wenzelm |
adapted to new-style theories;
|
file |
diff |
annotate
|
| Sat, 03 Nov 2001 01:41:26 +0100 |
wenzelm |
GPLed;
|
file |
diff |
annotate
|
| Fri, 12 Oct 2001 12:07:27 +0200 |
wenzelm |
fixed typid;
|
file |
diff |
annotate
|
| Wed, 29 Sep 1999 14:56:19 +0200 |
wenzelm |
Sign.defaultS;
|
file |
diff |
annotate
|
| Tue, 24 Mar 1998 15:53:47 +0100 |
oheimb |
improved checks
|
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
|
| Wed, 29 Oct 1997 14:23:49 +0100 |
oheimb |
debugging concerning sort variables
|
file |
diff |
annotate
|
| Mon, 27 Oct 1997 11:34:33 +0100 |
oheimb |
adapted domain and ax_ops package for name spaces
|
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
|
| 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
|