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
|
Fri, 03 Jul 2009 16:51:08 +0200 |
haftmann |
nominal.ML is nominal_datatype.ML
|
file |
diff |
annotate
|
Fri, 19 Jun 2009 17:23:21 +0200 |
haftmann |
discontinued ancient tradition to suffix certain ML module names with "_package"
|
file |
diff |
annotate
|
Sun, 26 Apr 2009 23:16:24 +0200 |
Christian Urban |
reorganised the section about fresh_star and added lemma pt_fresh_star_pi
|
file |
diff |
annotate
|
Sat, 25 Apr 2009 21:42:05 +0200 |
Christian Urban |
adapted permutation functions to new overloading syntax (the functions are still "unchecked" because they are used in conjunction with type-classes)
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 11:05:29 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
Wed, 04 Mar 2009 10:45:52 +0100 |
blanchet |
Merge.
|
file |
diff |
annotate
|
Thu, 26 Feb 2009 16:34:03 +0100 |
berghofe |
Added postprocessing rules for fresh_star.
|
file |
diff |
annotate
|
Wed, 25 Feb 2009 19:34:00 +0100 |
berghofe |
Added lemmas for normalizing freshness results involving fresh_star.
|
file |
diff |
annotate
|
Wed, 25 Feb 2009 11:02:25 +0100 |
berghofe |
Added equivariance lemmas for fresh_star.
|
file |
diff |
annotate
|
Sat, 14 Feb 2009 08:45:16 +0100 |
nipkow |
more finiteness changes
|
file |
diff |
annotate
|
Tue, 16 Dec 2008 20:32:41 +0000 |
Christian Urban |
changed the names of insert_eqvt and set_eqvt so that it is clear that they have preconditions
|
file |
diff |
annotate
|
Thu, 04 Dec 2008 14:43:33 +0100 |
haftmann |
cleaned up binding module and related code
|
file |
diff |
annotate
|
Tue, 21 Oct 2008 21:18:54 +0200 |
berghofe |
Added nominal_inductive2.ML
|
file |
diff |
annotate
|
Fri, 26 Sep 2008 14:51:27 +0200 |
berghofe |
Added some more lemmas that are useful in proof of strong induction rule.
|
file |
diff |
annotate
|
Mon, 22 Sep 2008 19:46:24 +0200 |
urbanc |
made the perm_simp tactic to understand options such as (no_asm)
|
file |
diff |
annotate
|
Wed, 27 Aug 2008 04:47:30 +0200 |
urbanc |
added equivariance lemmas for ex1 and the
|
file |
diff |
annotate
|
Sun, 27 Jul 2008 20:08:16 +0200 |
urbanc |
simplified a proof
|
file |
diff |
annotate
|
Fri, 27 Jun 2008 00:37:30 +0200 |
urbanc |
added a lemma to at_swap_simps
|
file |
diff |
annotate
|
Mon, 16 Jun 2008 17:54:39 +0200 |
wenzelm |
allE_Nil: only one copy, proven in regular theory source;
|
file |
diff |
annotate
|
Thu, 08 May 2008 04:20:08 +0200 |
urbanc |
added at_set_avoiding lemmas
|
file |
diff |
annotate
|
Wed, 07 May 2008 10:57:19 +0200 |
berghofe |
Adapted to encoding of sets as predicates
|
file |
diff |
annotate
|
Fri, 02 May 2008 22:43:14 +0200 |
urbanc |
added more infrastructure for fresh_star
|
file |
diff |
annotate
|
Fri, 02 May 2008 16:32:51 +0200 |
urbanc |
polished the proof for atm_prm_fresh and more lemmas for fresh_star
|
file |
diff |
annotate
|
Thu, 03 Apr 2008 11:48:48 +0200 |
urbanc |
added generalised definitions for freshness of sets of atoms
|
file |
diff |
annotate
|
Wed, 19 Mar 2008 22:50:42 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Mon, 18 Feb 2008 03:12:08 +0100 |
urbanc |
added eqvt-flag to subseteq-lemma
|
file |
diff |
annotate
|
Thu, 24 Jan 2008 11:23:11 +0100 |
berghofe |
Added lemma at_fin_set_fresh.
|
file |
diff |
annotate
|
Fri, 14 Sep 2007 13:32:07 +0200 |
urbanc |
reverted back to the old version of the equivariance lemma for ALL
|
file |
diff |
annotate
|
Thu, 13 Sep 2007 23:58:38 +0200 |
urbanc |
some cleaning up to do with contexts
|
file |
diff |
annotate
|
Thu, 13 Sep 2007 18:06:50 +0200 |
berghofe |
Added equivariance lemma for induct_implies.
|
file |
diff |
annotate
|
Thu, 06 Sep 2007 16:28:42 +0200 |
urbanc |
trivial cleaning up
|
file |
diff |
annotate
|
Wed, 11 Jul 2007 11:28:13 +0200 |
berghofe |
Adapted to new inductive definition package.
|
file |
diff |
annotate
|
Thu, 14 Jun 2007 23:04:36 +0200 |
wenzelm |
tuned proofs: avoid implicit prems;
|
file |
diff |
annotate
|
Thu, 31 May 2007 15:23:35 +0200 |
urbanc |
tuned the proof
|
file |
diff |
annotate
|
Thu, 31 May 2007 14:47:20 +0200 |
urbanc |
introduced symmetric variants of the lemmas for alpha-equivalence
|
file |
diff |
annotate
|
Sun, 20 May 2007 13:39:46 +0200 |
urbanc |
added lemma for permutations on strings
|
file |
diff |
annotate
|
Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
Thu, 03 May 2007 17:54:36 +0200 |
urbanc |
tuned some of the proofs and added the lemma fresh_bool
|
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, 26 Apr 2007 14:24:08 +0200 |
wenzelm |
eliminated unnamed infixes, tuned syntax;
|
file |
diff |
annotate
|
Tue, 24 Apr 2007 17:16:55 +0200 |
narboux |
fixes last commit
|
file |
diff |
annotate
|
Tue, 24 Apr 2007 16:44:11 +0200 |
narboux |
add two lemmas dealing with freshness on permutations.
|
file |
diff |
annotate
|
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
|
Sun, 02 Jul 2006 17:27:10 +0200 |
urbanc |
added more infrastructure for the recursion combinator
|
file |
diff |
annotate
|
Tue, 13 Jun 2006 15:07:47 +0200 |
paulson |
removal of the obsolete "infinite_nonempty"
|
file |
diff |
annotate
|
Mon, 12 Jun 2006 20:32:33 +0200 |
urbanc |
added lemma fresh_unit to Nominal.thy
|
file |
diff |
annotate
|
Mon, 12 Jun 2006 18:15:45 +0200 |
berghofe |
Removed comments around declaration of fresh_guess method.
|
file |
diff |
annotate
|
Fri, 09 Jun 2006 17:32:38 +0200 |
berghofe |
unique_names no longer set to false (thanks to improved naming
|
file |
diff |
annotate
|
Mon, 05 Jun 2006 19:09:40 +0200 |
urbanc |
added some further lemmas that deal with permutations and set-operators
|
file |
diff |
annotate
|
Mon, 05 Jun 2006 18:38:41 +0200 |
urbanc |
added the lemma perm_diff
|
file |
diff |
annotate
|
Thu, 01 Jun 2006 14:15:08 +0200 |
urbanc |
added the hack "reset NameSpace.unique_names" to Nominal.thy
|
file |
diff |
annotate
|
Sat, 20 May 2006 23:36:56 +0200 |
wenzelm |
primrec (unchecked);
|
file |
diff |
annotate
|
Mon, 15 May 2006 19:40:17 +0200 |
urbanc |
added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
|
file |
diff |
annotate
|
Sat, 13 May 2006 02:51:47 +0200 |
wenzelm |
defs (unchecked overloaded), including former primrec;
|
file |
diff |
annotate
|
Fri, 05 May 2006 18:09:53 +0200 |
urbanc |
added the lemma pt_fresh_bij2
|
file |
diff |
annotate
|
Fri, 05 May 2006 16:29:27 +0200 |
urbanc |
added the lemma abs_fun_eq' to the nominal theory,
|
file |
diff |
annotate
|
Fri, 28 Apr 2006 15:54:34 +0200 |
berghofe |
Renamed "nominal" theory to "Nominal".
|
file |
diff |
annotate
|
Thu, 27 Apr 2006 01:41:30 +0200 |
urbanc |
isar-keywords.el
|
file |
diff |
annotate
|
Sun, 26 Mar 2006 03:22:42 +0200 |
urbanc |
simplified the proof at_fin_set_supp
|
file |
diff |
annotate
|
Fri, 24 Mar 2006 15:15:08 +0100 |
urbanc |
tuned some proofs
|
file |
diff |
annotate
|
Wed, 08 Mar 2006 17:54:55 +0100 |
urbanc |
tuned some of the proofs about fresh_fun
|
file |
diff |
annotate
|
Wed, 01 Mar 2006 10:27:48 +0100 |
urbanc |
added initialisation-code for finite_guess
|
file |
diff |
annotate
|
Sun, 26 Feb 2006 22:25:17 +0100 |
urbanc |
replaced the lemma at_two by at_different;
|
file |
diff |
annotate
|
Thu, 23 Feb 2006 20:56:31 +0100 |
urbanc |
added lemmas
|
file |
diff |
annotate
|
Sun, 19 Feb 2006 17:18:39 +0100 |
urbanc |
added a few lemmas to do with permutation-equivalence for the
|
file |
diff |
annotate
|
Wed, 15 Feb 2006 19:11:10 +0100 |
urbanc |
added lemma pt_perm_compose'
|
file |
diff |
annotate
|
Sun, 22 Jan 2006 21:58:43 +0100 |
urbanc |
a fixme comments about abs_fun_if, which should be called perm_if
|
file |
diff |
annotate
|
Wed, 18 Jan 2006 02:48:58 +0100 |
urbanc |
fixed one proof that broke because of the changes
|
file |
diff |
annotate
|
Wed, 11 Jan 2006 18:20:59 +0100 |
berghofe |
Added theorem at_finite_select.
|
file |
diff |
annotate
|
Wed, 11 Jan 2006 17:12:30 +0100 |
urbanc |
added lemmas perm_empty, perm_insert to do with
|
file |
diff |
annotate
|
Tue, 10 Jan 2006 02:32:10 +0100 |
urbanc |
added the lemmas supp_char and supp_string
|
file |
diff |
annotate
|
Sat, 07 Jan 2006 11:43:42 +0100 |
urbanc |
added private datatype nprod (copy of prod) to be
|
file |
diff |
annotate
|
Thu, 05 Jan 2006 12:09:26 +0100 |
urbanc |
changed the name of the type "nOption" to "noption".
|
file |
diff |
annotate
|
Wed, 04 Jan 2006 20:20:25 +0100 |
urbanc |
added "fresh_singleton" lemma
|
file |
diff |
annotate
|
Thu, 22 Dec 2005 13:31:58 +0100 |
berghofe |
Tuned syntax for perm.
|
file |
diff |
annotate
|
Sun, 18 Dec 2005 14:36:42 +0100 |
urbanc |
improved the finite-support proof
|
file |
diff |
annotate
|
Mon, 05 Dec 2005 10:32:37 +0100 |
urbanc |
ISAR-fied two proofs
|
file |
diff |
annotate
|
Wed, 30 Nov 2005 12:28:47 +0100 |
urbanc |
changed \<sim> of permutation equality to \<triangleq>
|
file |
diff |
annotate
|
Wed, 30 Nov 2005 12:23:35 +0100 |
wenzelm |
fresh_unit_elim and fresh_prod_elim -- for nominal_induct;
|
file |
diff |
annotate
|
Mon, 28 Nov 2005 00:25:43 +0100 |
urbanc |
ISAR-fied two proofs about equality for abstraction functions.
|
file |
diff |
annotate
|
Sun, 27 Nov 2005 05:00:43 +0100 |
urbanc |
added the version of nominal.thy that contains
|
file |
diff |
annotate
|
Fri, 25 Nov 2005 14:51:39 +0100 |
urbanc |
added fsub.thy (poplmark challenge) to the examples
|
file |
diff |
annotate
|
Mon, 14 Nov 2005 13:59:58 +0100 |
urbanc |
added a few equivariance lemmas (they need to be automated
|
file |
diff |
annotate
|
Wed, 02 Nov 2005 16:37:39 +0100 |
berghofe |
Moved atom stuff to new file nominal_atoms.ML
|
file |
diff |
annotate
|
Tue, 01 Nov 2005 23:55:53 +0100 |
urbanc |
some minor tweaks in some proofs (nothing extraordinary)
|
file |
diff |
annotate
|
Sun, 30 Oct 2005 10:55:56 +0100 |
urbanc |
tuned my last commit
|
file |
diff |
annotate
|
Sun, 30 Oct 2005 10:37:57 +0100 |
urbanc |
simplified the abs_supp_approx proof and tuned some comments in
|
file |
diff |
annotate
|
Fri, 28 Oct 2005 16:43:46 +0200 |
urbanc |
Added (optional) arguments to the tactics
|
file |
diff |
annotate
|
Mon, 17 Oct 2005 17:40:34 +0200 |
urbanc |
deleted leading space in the definition of fresh
|
file |
diff |
annotate
|