| Sat, 13 Dec 2008 13:24:45 +0100 |
berghofe |
Modified nominal_primrec to make it work with local theories, unified syntax
|
file |
diff |
annotate
|
| Thu, 19 Jun 2008 15:47:26 +0200 |
urbanc |
slightly tuned
|
file |
diff |
annotate
|
| Thu, 22 May 2008 16:34:41 +0200 |
urbanc |
made the naming of the induction principles consistent: weak_induct is
|
file |
diff |
annotate
|
| Sat, 17 May 2008 21:46:22 +0200 |
wenzelm |
avoid undeclared variables within proofs;
|
file |
diff |
annotate
|
| Fri, 02 May 2008 18:42:17 +0200 |
urbanc |
added mising lemma
|
file |
diff |
annotate
|
| Tue, 08 Jan 2008 23:11:08 +0100 |
urbanc |
tuned proofs
|
file |
diff |
annotate
|
| Fri, 04 Jan 2008 09:34:11 +0100 |
urbanc |
adapted to new inversion rules
|
file |
diff |
annotate
|
| Mon, 08 Oct 2007 07:38:13 +0200 |
urbanc |
Isar-fied many proofs
|
file |
diff |
annotate
|
| Tue, 24 Jul 2007 20:34:11 +0200 |
urbanc |
cleaned up the proofs a bit
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:36:06 +0200 |
berghofe |
Renamed inductive2 to inductive.
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 23:04:36 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Thu, 31 May 2007 09:14:14 +0200 |
urbanc |
tuned the proof
|
file |
diff |
annotate
|
| Thu, 19 Apr 2007 16:38:59 +0200 |
berghofe |
nominal_inductive no longer proves equivariance.
|
file |
diff |
annotate
|
| Thu, 12 Apr 2007 15:46:12 +0200 |
urbanc |
tuned the proof of lemma pt_list_set_fresh (as suggested by Randy Pollack) and tuned the syntax for sub_contexts
|
file |
diff |
annotate
|
| Wed, 28 Mar 2007 19:16:11 +0200 |
berghofe |
- Renamed <predicate>_eqvt to <predicate>.eqvt
|
file |
diff |
annotate
|
| Wed, 28 Mar 2007 18:25:23 +0200 |
urbanc |
the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
|
file |
diff |
annotate
|
| Wed, 28 Mar 2007 17:27:44 +0200 |
urbanc |
adapted to new nominal_inductive
|
file |
diff |
annotate
|
| Wed, 28 Mar 2007 01:55:18 +0200 |
urbanc |
tuned proofs (taking full advantage of nominal_inductive)
|
file |
diff |
annotate
|
| Tue, 27 Mar 2007 17:57:05 +0200 |
berghofe |
Adapted to changes in nominal_inductive.
|
file |
diff |
annotate
|
| Tue, 13 Mar 2007 08:49:58 +0100 |
urbanc |
deleted function for defining candidates and used nominal_primrec instead
|
file |
diff |
annotate
|
| Tue, 06 Mar 2007 16:17:52 +0100 |
urbanc |
updated this file to the new infrastructure
|
file |
diff |
annotate
|
| Tue, 06 Mar 2007 15:28:22 +0100 |
urbanc |
major update of the nominal package; there is now an infrastructure
|
file |
diff |
annotate
|
| Wed, 07 Feb 2007 17:44:07 +0100 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
| 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
|