Sun, 07 May 2006 00:22:05 +0200 |
wenzelm |
removed 'concl is' patterns;
|
file |
diff |
annotate
|
Fri, 05 May 2006 17:17:21 +0200 |
krauss |
First usable version of the new function definition package (HOL/function_packake/...).
|
file |
diff |
annotate
|
Thu, 02 Feb 2006 10:24:06 +0100 |
krauss |
Exporting recdef's hints for use by new recdef package
|
file |
diff |
annotate
|
Fri, 27 Jan 2006 19:03:02 +0100 |
wenzelm |
moved theorem tags from Drule to PureThy;
|
file |
diff |
annotate
|
Sat, 21 Jan 2006 23:02:14 +0100 |
wenzelm |
simplified type attribute;
|
file |
diff |
annotate
|
Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
Sat, 14 Jan 2006 22:25:34 +0100 |
wenzelm |
generic attributes;
|
file |
diff |
annotate
|
Fri, 16 Dec 2005 09:00:11 +0100 |
haftmann |
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
|
file |
diff |
annotate
|
Fri, 09 Dec 2005 09:06:45 +0100 |
haftmann |
oriented result pairs in PureThy
|
file |
diff |
annotate
|
Wed, 19 Oct 2005 21:52:32 +0200 |
wenzelm |
removed obsolete add_recdef_old;
|
file |
diff |
annotate
|
Fri, 23 Sep 2005 09:00:19 +0200 |
haftmann |
temporarily re-introduced overwrite_warn
|
file |
diff |
annotate
|
Wed, 21 Sep 2005 17:25:32 +0200 |
haftmann |
introduces update_warn instead of overwrite_warn
|
file |
diff |
annotate
|
Tue, 20 Sep 2005 08:21:49 +0200 |
haftmann |
slight adaptions to library changes
|
file |
diff |
annotate
|
Thu, 15 Sep 2005 17:16:56 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
Tue, 13 Sep 2005 22:19:19 +0200 |
wenzelm |
tuned IsarThy.theorem_i;
|
file |
diff |
annotate
|
Mon, 05 Sep 2005 17:38:18 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
Tue, 16 Aug 2005 13:42:26 +0200 |
wenzelm |
OuterKeyword;
|
file |
diff |
annotate
|
Fri, 01 Jul 2005 14:14:40 +0200 |
berghofe |
Adapted to new interface of RecfunCodegen.add.
|
file |
diff |
annotate
|
Fri, 17 Jun 2005 18:35:27 +0200 |
wenzelm |
accomodate change of TheoryDataFun;
|
file |
diff |
annotate
|
Sat, 11 Jun 2005 22:15:48 +0200 |
wenzelm |
refer to name spaces values instead of names;
|
file |
diff |
annotate
|
Tue, 31 May 2005 11:53:13 +0200 |
wenzelm |
renamed cond_extern to extern;
|
file |
diff |
annotate
|
Wed, 13 Apr 2005 18:45:25 +0200 |
wenzelm |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
|
file |
diff |
annotate
|
Wed, 13 Apr 2005 18:34:22 +0200 |
wenzelm |
*** empty log message ***
|
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, 24 Jan 2005 18:07:10 +0100 |
berghofe |
Replaced xstring by thmref.
|
file |
diff |
annotate
|
Sun, 11 Jul 2004 20:33:22 +0200 |
wenzelm |
local_cla/simpset_of;
|
file |
diff |
annotate
|
Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
Fri, 17 Oct 2003 11:04:36 +0200 |
paulson |
Prevent recdef from looping when the inductio rule is simplified
|
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
|
Tue, 15 Jan 2002 00:08:51 +0100 |
wenzelm |
removed case_numbers (already covered by default);
|
file |
diff |
annotate
|
Fri, 11 Jan 2002 00:28:24 +0100 |
wenzelm |
clarified IsarThy.apply_theorems_i;
|
file |
diff |
annotate
|
Thu, 10 Jan 2002 01:11:43 +0100 |
wenzelm |
simplified IsarThy.theorem_i;
|
file |
diff |
annotate
|
Mon, 10 Dec 2001 15:34:15 +0100 |
berghofe |
Recursive equations to be used for code generation are now registered
|
file |
diff |
annotate
|
Wed, 05 Dec 2001 03:06:05 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 28 Nov 2001 00:46:26 +0100 |
wenzelm |
theory data: removed obsolete finish method;
|
file |
diff |
annotate
|
Thu, 08 Nov 2001 23:59:37 +0100 |
wenzelm |
theory data: finish method;
|
file |
diff |
annotate
|
Sun, 04 Nov 2001 20:56:59 +0100 |
wenzelm |
IsarThy.theorem_i (None, []);
|
file |
diff |
annotate
|
Wed, 31 Oct 2001 21:59:07 +0100 |
wenzelm |
IsarThy.theorem_i: no locale;
|
file |
diff |
annotate
|
Sat, 13 Oct 2001 20:31:34 +0200 |
wenzelm |
IsarThy.theorem_i Drule.internalK;
|
file |
diff |
annotate
|
Fri, 28 Sep 2001 19:21:26 +0200 |
wenzelm |
permissive option;
|
file |
diff |
annotate
|
Wed, 03 Jan 2001 21:25:23 +0100 |
wenzelm |
added recdef_tc(_i);
|
file |
diff |
annotate
|
Thu, 19 Oct 2000 01:47:50 +0200 |
wenzelm |
added tcs_of;
|
file |
diff |
annotate
|
Tue, 19 Sep 2000 23:52:00 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 15 Sep 2000 20:22:36 +0200 |
wenzelm |
added "congs" keyword;
|
file |
diff |
annotate
|
Fri, 15 Sep 2000 19:34:28 +0200 |
wenzelm |
"hints" made keyword again;
|
file |
diff |
annotate
|
Wed, 13 Sep 2000 22:28:50 +0200 |
wenzelm |
tuned recdef hints;
|
file |
diff |
annotate
|
Thu, 07 Sep 2000 20:51:07 +0200 |
wenzelm |
tuned msg;
|
file |
diff |
annotate
|
Wed, 06 Sep 2000 19:01:37 +0200 |
wenzelm |
make SML/NJ happy;
|
file |
diff |
annotate
|
Wed, 06 Sep 2000 16:54:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 05 Sep 2000 18:49:26 +0200 |
wenzelm |
recdef hints (attributes and modifiers);
|
file |
diff |
annotate
|
Fri, 18 Aug 2000 18:06:10 +0200 |
wenzelm |
removed obsolete add_recdef_x;
|
file |
diff |
annotate
|
Thu, 17 Aug 2000 18:31:12 +0200 |
nipkow |
installed recdef congs data
|
file |
diff |
annotate
|
Tue, 18 Apr 2000 14:54:08 +0200 |
wenzelm |
removed obsolete "simpset" keyword;
|
file |
diff |
annotate
|
Thu, 13 Apr 2000 17:49:42 +0200 |
wenzelm |
outer syntax: no simps;
|
file |
diff |
annotate
|
Sat, 01 Apr 2000 20:21:39 +0200 |
wenzelm |
recdef: admit names/atts;
|
file |
diff |
annotate
|
Thu, 30 Mar 2000 19:47:17 +0200 |
nipkow |
If all termination conditions are proved automatically,
|
file |
diff |
annotate
|
Wed, 15 Mar 2000 23:40:59 +0100 |
berghofe |
get_recdef now returns None instead of raising ERROR.
|
file |
diff |
annotate
|
Mon, 13 Mar 2000 13:18:59 +0100 |
wenzelm |
adapted to new PureThy.add_thms etc.;
|
file |
diff |
annotate
|