| Mon, 30 Sep 2013 13:20:44 +0200 |
wenzelm |
provide regular ML interface and use plain Syntax.read_prop/Syntax.check_prop (update by Manuel Eberl);
|
file |
diff |
annotate
|
| Tue, 10 Sep 2013 20:09:53 +0200 |
krauss |
added some examples and tests for fun_cases
|
file |
diff |
annotate
|
| Tue, 20 Sep 2011 01:32:04 +0200 |
krauss |
match types when applying mono_thm -- previous export generalizes type variables;
|
file |
diff |
annotate
|
| Tue, 22 Feb 2011 16:47:18 +0100 |
krauss |
dropped obsolete FIXMEs
|
file |
diff |
annotate
|
| Wed, 29 Dec 2010 17:34:41 +0100 |
wenzelm |
explicit file specifications -- avoid secondary load path;
|
file |
diff |
annotate
|
| Tue, 26 Oct 2010 12:19:01 +0200 |
krauss |
declare recursive equation as ".simps", in accordance with other packages
|
file |
diff |
annotate
|
| Mon, 25 Oct 2010 10:45:22 +0200 |
krauss |
some partial_function examples
|
file |
diff |
annotate
|
| Tue, 28 Sep 2010 09:54:07 +0200 |
krauss |
no longer declare .psimps rules as [simp].
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 15:45:33 +0200 |
krauss |
tolerate eta-variants in f_graph.cases (from inductive package); added test case;
|
file |
diff |
annotate
|
| Wed, 21 Apr 2010 15:37:39 +0200 |
krauss |
simplified example
|
file |
diff |
annotate
|
| Tue, 14 Oct 2008 13:24:07 +0200 |
nipkow |
added lemma
|
file |
diff |
annotate
|
| Mon, 17 Dec 2007 18:38:28 +0100 |
berghofe |
Adapted to changes in size function.
|
file |
diff |
annotate
|
| Wed, 24 Oct 2007 18:32:53 +0200 |
krauss |
tuned
|
file |
diff |
annotate
|
| Sat, 15 Sep 2007 19:27:40 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 16 Jul 2007 21:16:16 +0200 |
krauss |
updated
|
file |
diff |
annotate
|
| Mon, 11 Jun 2007 11:06:04 +0200 |
chaieb |
tuned Proof
|
file |
diff |
annotate
|
| Tue, 29 May 2007 14:03:49 +0200 |
krauss |
updated examples to include an instance of (lexicographic_order simp:...)
|
file |
diff |
annotate
|
| Wed, 18 Apr 2007 11:47:08 +0200 |
krauss |
proper header, added regression tests
|
file |
diff |
annotate
|
| Tue, 10 Apr 2007 08:19:20 +0200 |
krauss |
added example for definitions in local contexts
|
file |
diff |
annotate
|
| Wed, 21 Mar 2007 16:06:15 +0100 |
krauss |
Unified function syntax
|
file |
diff |
annotate
|
| Mon, 22 Jan 2007 17:29:43 +0100 |
krauss |
* Preliminary implementation of tail recursion
|
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
|
| Wed, 08 Nov 2006 09:08:54 +0100 |
krauss |
Made "termination by lexicographic_order" the default for "fun" definitions.
|
file |
diff |
annotate
|
| Wed, 18 Oct 2006 16:13:03 +0200 |
krauss |
Switched function package to use the new package for inductive predicates.
|
file |
diff |
annotate
|
| Thu, 14 Sep 2006 15:27:08 +0200 |
krauss |
Function package: Outside their domain functions now return "arbitrary".
|
file |
diff |
annotate
|
| Wed, 13 Sep 2006 12:37:13 +0200 |
krauss |
Removed debugging code imports...
|
file |
diff |
annotate
|
| Wed, 13 Sep 2006 12:05:50 +0200 |
krauss |
Major update to function package, including new syntax and the (only theoretical)
|
file |
diff |
annotate
|
| Mon, 31 Jul 2006 18:07:42 +0200 |
krauss |
Function package can now do automatic splits of overlapping datatype patterns
|
file |
diff |
annotate
|
| Mon, 19 Jun 2006 18:25:34 +0200 |
krauss |
Fixed name clash.
|
file |
diff |
annotate
|
| Tue, 06 Jun 2006 09:28:24 +0200 |
krauss |
HOL/Tools/function_package: imporoved handling of guards, added an example
|
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
|
| Sat, 27 May 2006 17:42:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 07 May 2006 00:00:13 +0200 |
krauss |
function-package: Changed record usage to make sml/nj happy...
|
file |
diff |
annotate
|
| Fri, 05 May 2006 18:39:16 +0200 |
krauss |
Added small example theory for new function package.
|
file |
diff |
annotate
|