| Sun, 08 Mar 2009 17:26:14 +0100 |
wenzelm |
moved basic algebra of long names from structure NameSpace to Long_Name;
|
file |
diff |
annotate
|
| Thu, 05 Mar 2009 12:08:00 +0100 |
wenzelm |
renamed NameSpace.base to NameSpace.base_name;
|
file |
diff |
annotate
|
| Sun, 01 Mar 2009 23:36:12 +0100 |
wenzelm |
use long names for old-style fold combinators;
|
file |
diff |
annotate
|
| Wed, 21 Jan 2009 16:47:04 +0100 |
haftmann |
binding replaces bstring
|
file |
diff |
annotate
|
| Wed, 31 Dec 2008 00:08:13 +0100 |
wenzelm |
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
|
file |
diff |
annotate
|
| Thu, 25 Sep 2008 20:34:15 +0200 |
wenzelm |
explicit checkpoint for low-level (global) theory operations, admits concurrent proofs;
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:09 +0200 |
wenzelm |
moved global pretty/string_of functions from Sign to Syntax;
|
file |
diff |
annotate
|
| Wed, 07 May 2008 10:59:38 +0200 |
berghofe |
Functions get_branching_types and get_arities now use fold instead of foldl/r.
|
file |
diff |
annotate
|
| Thu, 03 Apr 2008 17:50:50 +0200 |
berghofe |
Removed QuickAndDirty constructor from simproc_dist datatype.
|
file |
diff |
annotate
|
| Thu, 10 Jan 2008 19:18:14 +0100 |
berghofe |
Eliminated DatatypeAux.dest_TFree to avoid clashes
|
file |
diff |
annotate
|
| Mon, 17 Dec 2007 18:30:44 +0100 |
berghofe |
- Removed redundant head_len field in datatype_info
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 17:06:14 +0200 |
wenzelm |
proper Sign operations instead of Theory aliases;
|
file |
diff |
annotate
|
| Tue, 25 Sep 2007 12:16:08 +0200 |
haftmann |
datatype interpretators for size and datatype_realizer
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 23:29:33 +0200 |
wenzelm |
rep_thm/cterm/ctyp: removed obsolete sign field;
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 00:11:03 +0200 |
wenzelm |
removed obsolete sign_of/sign_of_thm;
|
file |
diff |
annotate
|
| Sat, 18 Nov 2006 00:20:29 +0100 |
haftmann |
cleanup
|
file |
diff |
annotate
|
| Fri, 13 Oct 2006 18:18:58 +0200 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| Sun, 11 Jun 2006 21:59:17 +0200 |
wenzelm |
avoid unqualified exception;
|
file |
diff |
annotate
|
| Sat, 11 Mar 2006 21:23:10 +0100 |
wenzelm |
got rid of type Sign.sg;
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:14 +0100 |
wenzelm |
simplified type attribute;
|
file |
diff |
annotate
|
| Fri, 09 Dec 2005 09:06:45 +0100 |
haftmann |
oriented result pairs in PureThy
|
file |
diff |
annotate
|
| Mon, 05 Dec 2005 00:38:07 +0100 |
berghofe |
Added store_thmss_atts to signature again.
|
file |
diff |
annotate
|
| Thu, 01 Dec 2005 18:39:08 +0100 |
berghofe |
Added new component "sorts" to record datatype_info.
|
file |
diff |
annotate
|
| Thu, 01 Dec 2005 08:28:02 +0100 |
haftmann |
oriented pairs theory * 'a to 'a * theory
|
file |
diff |
annotate
|
| Thu, 10 Nov 2005 20:57:11 +0100 |
wenzelm |
renamed Thm.cgoal_of to Thm.cprem_of;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2005 11:28:34 +0100 |
berghofe |
New function store_thmss_atts.
|
file |
diff |
annotate
|
| Wed, 02 Nov 2005 23:59:49 +0100 |
huffman |
fix spelling
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 22:27:46 +0200 |
wenzelm |
Logic.unprotect;
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 16:38:35 +0200 |
haftmann |
introduced AList module
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:16:56 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
| Mon, 05 Sep 2005 17:38:18 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
| Fri, 22 Jul 2005 11:55:11 +0200 |
berghofe |
Tuned comment.
|
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
|
| Tue, 07 Dec 2004 14:42:08 +0100 |
webertj |
comment added
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Tue, 08 Jun 2004 19:23:53 +0200 |
berghofe |
Added exception Datatype_Empty.
|
file |
diff |
annotate
|
| Mon, 26 Apr 2004 14:54:45 +0200 |
wenzelm |
use Syntax.is_identifier;
|
file |
diff |
annotate
|
| Wed, 13 Nov 2002 15:27:27 +0100 |
berghofe |
name_of_type now replaces non-identifiers by dummy names.
|
file |
diff |
annotate
|
| Thu, 10 Oct 2002 14:26:50 +0200 |
berghofe |
Reimplemented parts of datatype package dealing with datatypes involving
|
file |
diff |
annotate
|
| Fri, 31 Aug 2001 18:46:48 +0200 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Mon, 02 Oct 2000 14:21:12 +0200 |
wenzelm |
info: weak_case_cong;
|
file |
diff |
annotate
|
| Wed, 30 Aug 2000 13:55:26 +0200 |
berghofe |
New function name_of_typ.
|
file |
diff |
annotate
|
| Mon, 13 Mar 2000 13:22:31 +0100 |
wenzelm |
adapted to new PureThy.add_thms etc.;
|
file |
diff |
annotate
|
| Fri, 10 Mar 2000 01:13:37 +0100 |
wenzelm |
type descr;
|
file |
diff |
annotate
|
| Wed, 01 Mar 2000 20:48:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 27 Feb 2000 15:26:47 +0100 |
wenzelm |
HOLogic.dest_conj;
|
file |
diff |
annotate
|
| Fri, 16 Jul 1999 12:14:04 +0200 |
berghofe |
- Datatype package now also supports arbitrarily branching datatypes
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 16:53:46 +0100 |
wenzelm |
Theory.sign_of;
|
file |
diff |
annotate
|
| Tue, 12 Jan 1999 13:54:51 +0100 |
wenzelm |
eliminated tthm type and Attribute structure;
|
file |
diff |
annotate
|
| Mon, 16 Nov 1998 11:14:02 +0100 |
wenzelm |
Attribute.tthms_of;
|
file |
diff |
annotate
|
| Fri, 16 Oct 1998 18:54:55 +0200 |
berghofe |
- Changed structure of name spaces
|
file |
diff |
annotate
|
| Fri, 24 Jul 1998 12:50:06 +0200 |
berghofe |
New datatype definition package
|
file |
diff |
annotate
|