| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Wed, 15 Nov 2006 16:23:55 +0100 |
urbanc |
replaced exists_fresh lemma with a version formulated with obtains;
|
file |
diff |
annotate
|
| Mon, 30 Oct 2006 13:07:51 +0100 |
urbanc |
new file for defining functions in the lambda-calculus
|
file |
diff |
annotate
|
| Sun, 02 Jul 2006 17:27:10 +0200 |
urbanc |
added more infrastructure for the recursion combinator
|
file |
diff |
annotate
|
| Sat, 20 May 2006 23:36:56 +0200 |
wenzelm |
primrec (unchecked);
|
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
|
| Fri, 28 Apr 2006 15:58:30 +0200 |
berghofe |
Capitalized theory names.
|
file |
diff |
annotate
|
| Wed, 08 Mar 2006 18:00:00 +0100 |
urbanc |
deleted some proofs "on comment"
|
file |
diff |
annotate
|
| Wed, 11 Jan 2006 18:38:32 +0100 |
urbanc |
changes to make use of the new induction principle proved by
|
file |
diff |
annotate
|
| Wed, 11 Jan 2006 17:07:57 +0100 |
urbanc |
tuned proofs
|
file |
diff |
annotate
|
| Sat, 07 Jan 2006 13:50:38 +0100 |
urbanc |
another change for the new induct-method
|
file |
diff |
annotate
|
| Sat, 07 Jan 2006 11:36:58 +0100 |
urbanc |
changed PRO_RED proof to conform with the new induction rules
|
file |
diff |
annotate
|
| Sun, 11 Dec 2005 11:57:01 +0100 |
urbanc |
ISAR-fied some proofs
|
file |
diff |
annotate
|
| Sun, 11 Dec 2005 01:21:26 +0100 |
urbanc |
completed the sn proof and changed the manual
|
file |
diff |
annotate
|
| Fri, 09 Dec 2005 12:38:49 +0100 |
urbanc |
tuned
|
file |
diff |
annotate
|
| Sun, 04 Dec 2005 12:40:39 +0100 |
urbanc |
tuned
|
file |
diff |
annotate
|
| Sun, 04 Dec 2005 12:14:27 +0100 |
urbanc |
added an Isar-proof for the abs_ALL lemma
|
file |
diff |
annotate
|
| Thu, 01 Dec 2005 06:28:41 +0100 |
urbanc |
initial cleanup to use the new induction method
|
file |
diff |
annotate
|
| Mon, 28 Nov 2005 05:03:00 +0100 |
urbanc |
some small tuning
|
file |
diff |
annotate
|
| Sun, 27 Nov 2005 04:59:20 +0100 |
urbanc |
cleaned up all examples so that they work with the
|
file |
diff |
annotate
|
| Mon, 07 Nov 2005 15:19:03 +0100 |
urbanc |
Initial commit.
|
file |
diff |
annotate
|