| Thu, 26 May 2016 17:51:22 +0200 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| Tue, 03 Sep 2013 01:12:40 +0200 |
wenzelm |
tuned proofs -- clarified flow of facts wrt. calculation;
|
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
|
| Wed, 05 Sep 2012 20:19:37 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Mon, 21 Feb 2011 17:43:23 +0100 |
wenzelm |
modernized specifications;
|
file |
diff |
annotate
|
| Sat, 17 Oct 2009 14:43:18 +0200 |
wenzelm |
eliminated hard tabulators, guessing at each author's individual tab-width;
|
file |
diff |
annotate
|
| Mon, 21 Sep 2009 15:02:23 +0200 |
Christian Urban |
tuned some proofs
|
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, 28 Aug 2008 17:54:18 +0200 |
krauss |
more function -> fun
|
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
|
| Wed, 16 Apr 2008 02:25:06 +0200 |
urbanc |
removed test artefacts
|
file |
diff |
annotate
|
| Mon, 14 Apr 2008 21:44:53 +0200 |
wenzelm |
avoid duplicate fact bindings;
|
file |
diff |
annotate
|
| Fri, 19 Oct 2007 23:21:08 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Sun, 12 Aug 2007 18:53:03 +0200 |
wenzelm |
added type constraints to resolve syntax ambiguities;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2007 14:45:36 +0200 |
narboux |
undo a change in last commit : give a single name to the inversion lemmas for the same inductive type
|
file |
diff |
annotate
|
| Mon, 30 Jul 2007 10:39:12 +0200 |
urbanc |
updated some of the definitions and proofs
|
file |
diff |
annotate
|
| Wed, 11 Jul 2007 11:36:06 +0200 |
berghofe |
Renamed inductive2 to inductive.
|
file |
diff |
annotate
|
| Thu, 21 Jun 2007 13:49:27 +0200 |
narboux |
fine tune automatic generation of inversion lemmas
|
file |
diff |
annotate
|
| Thu, 14 Jun 2007 23:04:36 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
| Wed, 13 Jun 2007 12:22:02 +0200 |
urbanc |
added the Q_Unit rule (was missing) and adjusted the proof accordingly
|
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
|
| 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
|
| Sat, 07 Apr 2007 11:05:25 +0200 |
narboux |
perm_simp can now simplify using the rules (a,b) o a = b and (a,b) o b = a
|
file |
diff |
annotate
|
| Wed, 04 Apr 2007 19:56:25 +0200 |
narboux |
add a few details in the Fst and Snd cases of unicity proof
|
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 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
|
| Thu, 22 Mar 2007 16:34:03 +0100 |
krauss |
fixed function syntax
|
file |
diff |
annotate
|
| Thu, 22 Mar 2007 10:35:12 +0100 |
urbanc |
tuned some proofs
|
file |
diff |
annotate
|
| Wed, 21 Mar 2007 16:06:15 +0100 |
krauss |
Unified function syntax
|
file |
diff |
annotate
|
| Tue, 06 Mar 2007 16:40:32 +0100 |
narboux |
correct typo in latex output
|
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
|
| Fri, 02 Feb 2007 17:16:16 +0100 |
urbanc |
added an infrastructure that allows the user to declare lemmas to be equivariance lemmas; the intention is to use these lemmas in automated tools but also can be employed by the user
|
file |
diff |
annotate
|
| Wed, 17 Jan 2007 19:29:55 +0100 |
urbanc |
tuned a bit the proofs
|
file |
diff |
annotate
|
| Tue, 16 Jan 2007 13:59:08 +0100 |
urbanc |
formalisation of Crary's chapter on logical relations
|
file |
diff |
annotate
|