| Tue, 24 Apr 2007 14:02:16 +0200 |
narboux |
oups : wrong commit
|
file |
diff |
annotate
|
| Tue, 24 Apr 2007 14:01:23 +0200 |
narboux |
adds op in front of an infix to fix SML compilation
|
file |
diff |
annotate
|
| Mon, 23 Apr 2007 18:38:42 +0200 |
urbanc |
simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)
|
file |
diff |
annotate
|
| Sat, 21 Apr 2007 01:34:15 +0200 |
urbanc |
tuned the setup of fresh_fun
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 00:28:07 +0200 |
urbanc |
declared lemmas true_eqvt and false_eqvt to be equivariant (suggested by samth at ccs.neu.edu)
|
file |
diff |
annotate
|
| Thu, 19 Apr 2007 16:27:53 +0200 |
narboux |
add a tactic to generate fresh names
|
file |
diff |
annotate
|
| Mon, 16 Apr 2007 07:32:23 +0200 |
urbanc |
improved the equivariance lemmas for the quantifiers; had to export the lemma eqvt_force_add and eqvt_force_del in the thmdecls
|
file |
diff |
annotate
|
| Mon, 16 Apr 2007 06:45:22 +0200 |
urbanc |
added a more usuable lemma for dealing with fresh_fun
|
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:36:35 +0200 |
urbanc |
tuned slightly the previous commit
|
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
|
| Tue, 03 Apr 2007 17:05:52 +0200 |
narboux |
remove the lemma swap_fun which was not needed
|
file |
diff |
annotate
|
| Tue, 27 Mar 2007 19:39:40 +0200 |
urbanc |
added extended the lemma for equivariance of freshness
|
file |
diff |
annotate
|
| Sun, 25 Mar 2007 15:15:07 +0200 |
urbanc |
moving lemmas into appropriate sections
|
file |
diff |
annotate
|
| Fri, 23 Mar 2007 10:50:03 +0100 |
urbanc |
added the permutation operation on options to the list of equivariance lemmas
|
file |
diff |
annotate
|
| Thu, 22 Mar 2007 14:26:05 +0100 |
urbanc |
corrected the lemmas min_nat_eqvt and min_int_eqvt
|
file |
diff |
annotate
|
| Fri, 16 Mar 2007 17:09:18 +0100 |
urbanc |
added eqvt-lemmas for integers and eqvt-tagged the lemma append_eqvt
|
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
|
| Thu, 15 Feb 2007 18:18:21 +0100 |
narboux |
start adding the attribute eqvt to some lemmas of the nominal library
|
file |
diff |
annotate
|
| Tue, 13 Feb 2007 18:17:28 +0100 |
berghofe |
Added new file nominal_inductive.ML
|
file |
diff |
annotate
|
| Tue, 06 Feb 2007 00:41:54 +0100 |
urbanc |
moved the infrastructure from the nominal_tags file to nominal_thmdecls
|
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
|
| Mon, 27 Nov 2006 12:10:51 +0100 |
berghofe |
Implemented new "nominal_primrec" command for defining
|
file |
diff |
annotate
|
| Fri, 17 Nov 2006 17:32:30 +0100 |
urbanc |
added an intro lemma for freshness of products; set up
|
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, 13 Nov 2006 12:10:49 +0100 |
wenzelm |
added fresh_prodD, which is included fresh_prodD into mksimps setup;
|
file |
diff |
annotate
|
| Fri, 13 Oct 2006 15:01:34 +0200 |
urbanc |
added the missing freshness-lemmas for nat, int, char and string and
|
file |
diff |
annotate
|
| Sun, 01 Oct 2006 18:29:26 +0200 |
wenzelm |
moved theory Infinite_Set to Library;
|
file |
diff |
annotate
|
| Wed, 16 Aug 2006 16:44:41 +0200 |
urbanc |
added missing supp_nat lemma
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 15:22:54 +0200 |
berghofe |
- nominal_permeq.ML is now loaded before nominal_package.ML
|
file |
diff |
annotate
|