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
|
Fri, 08 Oct 1999 15:08:23 +0200 |
wenzelm |
return stored thms with proper naming in derivation;
|
file |
diff |
annotate
|
Wed, 18 Aug 1999 18:44:20 +0200 |
paulson |
from Konrad: support for schematic definitions
|
file |
diff |
annotate
|
Mon, 28 Jun 1999 21:48:36 +0200 |
wenzelm |
cond_extern_table;
|
file |
diff |
annotate
|
Tue, 25 May 1999 20:24:10 +0200 |
wenzelm |
formal comments (still dummy);
|
file |
diff |
annotate
|
Mon, 24 May 1999 21:57:13 +0200 |
wenzelm |
outer syntax keyword classification;
|
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:10:35 +0200 |
wenzelm |
peoper defer_recdef interface;
|
file |
diff |
annotate
|
Tue, 27 Apr 1999 10:50:08 +0200 |
wenzelm |
proper quiet_mode;
|
file |
diff |
annotate
|
Thu, 22 Apr 1999 12:50:39 +0200 |
wenzelm |
add_recdef: actual simpset;
|
file |
diff |
annotate
|
Tue, 20 Apr 1999 15:20:27 +0200 |
wenzelm |
temporarily fake quiet_mode;
|
file |
diff |
annotate
|
Fri, 16 Apr 1999 14:49:09 +0200 |
wenzelm |
'HOL/recdef' theory data;
|
file |
diff |
annotate
|
Wed, 14 Apr 1999 19:05:10 +0200 |
wenzelm |
Wrapper module for Konrad Slind's TFL package.
|
file |
diff |
annotate
|