| Thu, 26 May 2016 17:51:22 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2013 16:25:47 +0200 |
wenzelm |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
file |
diff |
annotate
|
| Sun, 16 Jan 2011 15:53:03 +0100 |
wenzelm |
tuned headers;
|
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
|
| Mon, 28 Jan 2008 08:14:31 +0100 |
urbanc |
tuned the proof of the substitution lemma
|
file |
diff |
annotate
|
| Fri, 04 Jan 2008 09:34:11 +0100 |
urbanc |
adapted to new inversion rules
|
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
|
| Fri, 27 Apr 2007 18:50:27 +0200 |
urbanc |
tuned some proofs in CR and properly included CR_Takahashi
|
file |
diff |
annotate
|
| Thu, 19 Apr 2007 16:38:59 +0200 |
berghofe |
nominal_inductive no longer proves equivariance.
|
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 17:27:44 +0200 |
urbanc |
adapted to new nominal_inductive
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 14:05:43 +0100 |
urbanc |
adapted function definitions to new syntax
|
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
|
| Tue, 14 Nov 2006 22:16:57 +0100 |
wenzelm |
inductive2: canonical specification syntax;
|
file |
diff |
annotate
|
| Wed, 01 Nov 2006 19:07:37 +0100 |
urbanc |
changed a misplaced "also" to a "moreover" (caused a loop somehow)
|
file |
diff |
annotate
|
| Wed, 01 Nov 2006 16:11:31 +0100 |
urbanc |
changed to use Lam_Funs
|
file |
diff |
annotate
|
| Tue, 24 Oct 2006 12:02:53 +0200 |
urbanc |
adapted to Stefan's new inductive package
|
file |
diff |
annotate
|
| Tue, 10 Oct 2006 16:26:59 +0200 |
urbanc |
made some proof look more like the ones in Barendregt
|
file |
diff |
annotate
|
| Mon, 11 Sep 2006 21:35:19 +0200 |
wenzelm |
induct method: renamed 'fixing' to 'arbitrary';
|
file |
diff |
annotate
|
| Fri, 28 Apr 2006 15:58:30 +0200 |
berghofe |
Capitalized theory names.
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 01:41:30 +0200 |
urbanc |
isar-keywords.el
|
file |
diff |
annotate
|
| Thu, 02 Mar 2006 16:01:06 +0100 |
urbanc |
fixed the bugs itroduced by the previous commit
|
file |
diff |
annotate
|
| Thu, 02 Mar 2006 15:43:22 +0100 |
urbanc |
made some small changes to generate nicer latex-output
|
file |
diff |
annotate
|
| Wed, 01 Feb 2006 01:05:17 +0100 |
urbanc |
- renamed some lemmas (some had names coming from ancient
|
file |
diff |
annotate
|
| Tue, 24 Jan 2006 13:28:06 +0100 |
urbanc |
the additional freshness-condition in the one-induction
|
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
|
| Fri, 09 Dec 2005 12:38:49 +0100 |
urbanc |
tuned
|
file |
diff |
annotate
|
| Sun, 04 Dec 2005 12:14:03 +0100 |
urbanc |
tuning
|
file |
diff |
annotate
|
| Thu, 01 Dec 2005 05:20:13 +0100 |
urbanc |
cleaned up further the proofs (diamond still needs work);
|
file |
diff |
annotate
|
| Wed, 30 Nov 2005 17:56:08 +0100 |
urbanc |
modified almost everything for the new nominal_induct
|
file |
diff |
annotate
|
| Mon, 28 Nov 2005 05:03:00 +0100 |
urbanc |
some small tuning
|
file |
diff |
annotate
|
| Mon, 07 Nov 2005 15:19:03 +0100 |
urbanc |
Initial commit.
|
file |
diff |
annotate
|