| Fri, 20 Sep 2024 19:51:08 +0200 |
wenzelm |
standardize mixfix annotations via "isabelle update -a -u mixfix_cartouches" --- to simplify systematic editing;
|
file |
diff |
annotate
|
| Wed, 24 Apr 2024 20:56:26 +0100 |
paulson |
More tidying of proofs
|
file |
diff |
annotate
|
| Fri, 18 Aug 2017 20:47:47 +0200 |
wenzelm |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
file |
diff |
annotate
|
| 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
|
| 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, 22 May 2008 16:34:41 +0200 |
urbanc |
made the naming of the induction principles consistent: weak_induct is
|
file |
diff |
annotate
|
| Fri, 02 May 2008 02:17:07 +0200 |
urbanc |
extended to be a library of general facts about the lambda calculus
|
file |
diff |
annotate
|
| Tue, 01 Jan 2008 07:28:20 +0100 |
urbanc |
tuned proofs and comments
|
file |
diff |
annotate
|
| Thu, 03 May 2007 19:00:28 +0200 |
urbanc |
deleted some unnecessary type-annotations
|
file |
diff |
annotate
|
| Wed, 02 May 2007 01:42:23 +0200 |
urbanc |
tuned some proofs and changed variable names in some definitions of Nominal.thy
|
file |
diff |
annotate
|
| Wed, 28 Mar 2007 17:27:44 +0200 |
urbanc |
adapted to new nominal_inductive
|
file |
diff |
annotate
|
| Wed, 21 Mar 2007 16:06:15 +0100 |
krauss |
Unified function syntax
|
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
|
| Mon, 27 Nov 2006 14:50:21 +0100 |
urbanc |
added the function for free variables of a lambda-term, which is a
|
file |
diff |
annotate
|
| Mon, 27 Nov 2006 14:05:43 +0100 |
urbanc |
adapted function definitions to new syntax
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 02:20:03 +0100 |
wenzelm |
more robust syntax for definition/abbreviation/notation;
|
file |
diff |
annotate
|
| Mon, 30 Oct 2006 13:07:51 +0100 |
urbanc |
new file for defining functions in the lambda-calculus
|
file |
diff |
annotate
|