| Fri, 13 Mar 2009 23:50:05 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Fri, 13 Mar 2009 19:58:26 +0100 |
wenzelm |
unified type Proof.method and pervasive METHOD combinators;
|
file |
diff |
annotate
|
| Wed, 05 Dec 2007 14:36:58 +0100 |
krauss |
methods "relation" and "lexicographic_order" do not insist on applying the "f.termination" rule of a function.
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 10:06:11 +0200 |
krauss |
definition lookup via terms, not names. Methods "relation" and "lexicographic_order"
|
file |
diff |
annotate
|
| Thu, 22 Mar 2007 13:36:55 +0100 |
krauss |
cleanup
|
file |
diff |
annotate
|
| Mon, 18 Dec 2006 08:21:35 +0100 |
haftmann |
switched argument order in *.syntax lifters
|
file |
diff |
annotate
|
| Wed, 13 Dec 2006 14:52:50 +0100 |
krauss |
simplified
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 15:44:51 +0100 |
wenzelm |
simplified method setup;
|
file |
diff |
annotate
|
| Mon, 13 Nov 2006 13:51:22 +0100 |
krauss |
replaced "auto_term" by the simpler method "relation", which does not try
|
file |
diff |
annotate
|
| Thu, 26 Oct 2006 15:16:31 +0200 |
krauss |
removed free "x" from termination goal...
|
file |
diff |
annotate
|
| Sat, 07 Oct 2006 01:31:01 +0200 |
wenzelm |
tuned method syntax: polymorhic term argument;
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:26:49 +0200 |
wenzelm |
use proper RecdefPackage.get_hints;
|
file |
diff |
annotate
|
| Mon, 05 Jun 2006 14:26:07 +0200 |
krauss |
HOL/Tools/function_package: Added support for mutual recursive definitions.
|
file |
diff |
annotate
|
| Thu, 11 May 2006 11:11:05 +0200 |
krauss |
Fix: Auto term must apply wf-intro rules repeatedly.
|
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
|