| Mon, 02 May 2005 13:30:36 +0200 |
paulson |
fixed reference to top-level
|
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, 03 May 2004 23:22:17 +0200 |
schirmer |
reimplementation of HOL records; only one type is created for
|
file |
diff |
annotate
|
| Mon, 26 Apr 2004 14:53:29 +0200 |
wenzelm |
use ThmDatabase.is_ml_identifier;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2004 18:45:56 +0200 |
berghofe |
Replaced quote by Library.quote, since quote now refers to Symbol.quote
|
file |
diff |
annotate
|
| Fri, 14 Dec 2001 22:26:55 +0100 |
wenzelm |
record: mixfix;
|
file |
diff |
annotate
|
| Wed, 14 Nov 2001 18:44:27 +0100 |
wenzelm |
inductive: removed con_defs;
|
file |
diff |
annotate
|
| Sun, 04 Nov 2001 21:12:03 +0100 |
wenzelm |
tuned comment;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2001 20:25:19 +0200 |
wenzelm |
improved internal interface of typedef;
|
file |
diff |
annotate
|
| Tue, 16 Oct 2001 17:52:07 +0200 |
wenzelm |
TypedefPackage.add_typedef_no_result;
|
file |
diff |
annotate
|
| Fri, 28 Sep 2001 19:19:26 +0200 |
wenzelm |
inductive: no collective atts;
|
file |
diff |
annotate
|
| Tue, 05 Sep 2000 18:48:41 +0200 |
wenzelm |
RecdefPackage.add_recdef_old;
|
file |
diff |
annotate
|
| Fri, 05 May 2000 22:29:02 +0200 |
wenzelm |
added scan_to_id (used to be in Pure/section_utils.ML);
|
file |
diff |
annotate
|
| Sat, 01 Apr 2000 20:21:39 +0200 |
wenzelm |
recdef: admit names/atts;
|
file |
diff |
annotate
|
| Thu, 30 Mar 2000 19:45:18 +0200 |
nipkow |
mod in recdef allows to access the correct simpset via simpset().
|
file |
diff |
annotate
|
| Wed, 12 May 1999 17:26:56 +0200 |
wenzelm |
strip_quotes replaced by unenclose;
|
file |
diff |
annotate
|
| Tue, 04 May 1999 16:18:16 +0200 |
wenzelm |
add_recdef: removed names / attributes;
|
file |
diff |
annotate
|
| Fri, 30 Apr 1999 18:09:33 +0200 |
wenzelm |
separated recdef / defer_recdef;
|
file |
diff |
annotate
|
| Tue, 27 Apr 1999 10:51:16 +0200 |
wenzelm |
adapted add_inductive, add_record;
|
file |
diff |
annotate
|
| Fri, 23 Apr 1999 12:22:30 +0200 |
paulson |
Now for recdefs that omit the WF relation
|
file |
diff |
annotate
|
| Thu, 22 Apr 1999 12:49:34 +0200 |
wenzelm |
recdef adapted to RecdefPackage.add_recdef;
|
file |
diff |
annotate
|
| Wed, 14 Apr 1999 14:44:04 +0200 |
wenzelm |
intrs: names and atts;
|
file |
diff |
annotate
|
| Wed, 17 Mar 1999 13:47:04 +0100 |
wenzelm |
adapted rep_datatype;
|
file |
diff |
annotate
|
| Thu, 11 Mar 1999 21:56:22 +0100 |
wenzelm |
primrec: empty attributes;
|
file |
diff |
annotate
|
| Tue, 12 Jan 1999 16:42:21 +0100 |
wenzelm |
get_tthms witness theorems;
|
file |
diff |
annotate
|
| Mon, 28 Dec 1998 16:46:15 +0100 |
paulson |
replaced obsolete "trim" by "strip_quotes"
|
file |
diff |
annotate
|
| Wed, 21 Oct 1998 17:46:00 +0200 |
berghofe |
Changed syntax of rep_datatype and inductive: Theorems
|
file |
diff |
annotate
|
| Fri, 16 Oct 1998 18:50:20 +0200 |
berghofe |
Changed structure of name spaces for datatypes.
|
file |
diff |
annotate
|
| Thu, 30 Jul 1998 23:14:41 +0200 |
berghofe |
Fixed primrec.
|
file |
diff |
annotate
|