| 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
|