src/HOL/Nominal/Nominal.thy
Tue, 24 Apr 2007 14:02:16 +0200 narboux oups : wrong commit
Tue, 24 Apr 2007 14:01:23 +0200 narboux adds op in front of an infix to fix SML compilation
Mon, 23 Apr 2007 18:38:42 +0200 urbanc simplified the proof of pt_set_eqvt (as suggested by Randy Pollack)
Sat, 21 Apr 2007 01:34:15 +0200 urbanc tuned the setup of fresh_fun
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)
Thu, 19 Apr 2007 16:27:53 +0200 narboux add a tactic to generate fresh names
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
Mon, 16 Apr 2007 06:45:22 +0200 urbanc added a more usuable lemma for dealing with fresh_fun
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
Sat, 07 Apr 2007 11:36:35 +0200 urbanc tuned slightly the previous commit
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
Tue, 03 Apr 2007 17:05:52 +0200 narboux remove the lemma swap_fun which was not needed
Tue, 27 Mar 2007 19:39:40 +0200 urbanc added extended the lemma for equivariance of freshness
Sun, 25 Mar 2007 15:15:07 +0200 urbanc moving lemmas into appropriate sections
Fri, 23 Mar 2007 10:50:03 +0100 urbanc added the permutation operation on options to the list of equivariance lemmas
Thu, 22 Mar 2007 14:26:05 +0100 urbanc corrected the lemmas min_nat_eqvt and min_int_eqvt
Fri, 16 Mar 2007 17:09:18 +0100 urbanc added eqvt-lemmas for integers and eqvt-tagged the lemma append_eqvt
Tue, 06 Mar 2007 15:28:22 +0100 urbanc major update of the nominal package; there is now an infrastructure
Thu, 15 Feb 2007 18:18:21 +0100 narboux start adding the attribute eqvt to some lemmas of the nominal library
Tue, 13 Feb 2007 18:17:28 +0100 berghofe Added new file nominal_inductive.ML
Tue, 06 Feb 2007 00:41:54 +0100 urbanc moved the infrastructure from the nominal_tags file to nominal_thmdecls
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
Mon, 27 Nov 2006 12:10:51 +0100 berghofe Implemented new "nominal_primrec" command for defining
Fri, 17 Nov 2006 17:32:30 +0100 urbanc added an intro lemma for freshness of products; set up
Wed, 15 Nov 2006 16:23:55 +0100 urbanc replaced exists_fresh lemma with a version formulated with obtains;
Mon, 13 Nov 2006 12:10:49 +0100 wenzelm added fresh_prodD, which is included fresh_prodD into mksimps setup;
Fri, 13 Oct 2006 15:01:34 +0200 urbanc added the missing freshness-lemmas for nat, int, char and string and
Sun, 01 Oct 2006 18:29:26 +0200 wenzelm moved theory Infinite_Set to Library;
Wed, 16 Aug 2006 16:44:41 +0200 urbanc added missing supp_nat lemma
Tue, 04 Jul 2006 15:22:54 +0200 berghofe - nominal_permeq.ML is now loaded before nominal_package.ML
Sun, 02 Jul 2006 17:27:10 +0200 urbanc added more infrastructure for the recursion combinator
Tue, 13 Jun 2006 15:07:47 +0200 paulson removal of the obsolete "infinite_nonempty"
Mon, 12 Jun 2006 20:32:33 +0200 urbanc added lemma fresh_unit to Nominal.thy
Mon, 12 Jun 2006 18:15:45 +0200 berghofe Removed comments around declaration of fresh_guess method.
Fri, 09 Jun 2006 17:32:38 +0200 berghofe unique_names no longer set to false (thanks to improved naming
Mon, 05 Jun 2006 19:09:40 +0200 urbanc added some further lemmas that deal with permutations and set-operators
Mon, 05 Jun 2006 18:38:41 +0200 urbanc added the lemma perm_diff
Thu, 01 Jun 2006 14:15:08 +0200 urbanc added the hack "reset NameSpace.unique_names" to Nominal.thy
Sat, 20 May 2006 23:36:56 +0200 wenzelm primrec (unchecked);
Mon, 15 May 2006 19:40:17 +0200 urbanc added the lemmas pt_fresh_aux and pt_fresh_aux_ineq
Sat, 13 May 2006 02:51:47 +0200 wenzelm defs (unchecked overloaded), including former primrec;
Fri, 05 May 2006 18:09:53 +0200 urbanc added the lemma pt_fresh_bij2
Fri, 05 May 2006 16:29:27 +0200 urbanc added the lemma abs_fun_eq' to the nominal theory,
Fri, 28 Apr 2006 15:54:34 +0200 berghofe Renamed "nominal" theory to "Nominal".
Thu, 27 Apr 2006 01:41:30 +0200 urbanc isar-keywords.el
Sun, 26 Mar 2006 03:22:42 +0200 urbanc simplified the proof at_fin_set_supp
Fri, 24 Mar 2006 15:15:08 +0100 urbanc tuned some proofs
Wed, 08 Mar 2006 17:54:55 +0100 urbanc tuned some of the proofs about fresh_fun
Wed, 01 Mar 2006 10:27:48 +0100 urbanc added initialisation-code for finite_guess
Sun, 26 Feb 2006 22:25:17 +0100 urbanc replaced the lemma at_two by at_different;
Thu, 23 Feb 2006 20:56:31 +0100 urbanc added lemmas
Sun, 19 Feb 2006 17:18:39 +0100 urbanc added a few lemmas to do with permutation-equivalence for the
Wed, 15 Feb 2006 19:11:10 +0100 urbanc added lemma pt_perm_compose'
Sun, 22 Jan 2006 21:58:43 +0100 urbanc a fixme comments about abs_fun_if, which should be called perm_if
Wed, 18 Jan 2006 02:48:58 +0100 urbanc fixed one proof that broke because of the changes
Wed, 11 Jan 2006 18:20:59 +0100 berghofe Added theorem at_finite_select.
Wed, 11 Jan 2006 17:12:30 +0100 urbanc added lemmas perm_empty, perm_insert to do with
Tue, 10 Jan 2006 02:32:10 +0100 urbanc added the lemmas supp_char and supp_string
Sat, 07 Jan 2006 11:43:42 +0100 urbanc added private datatype nprod (copy of prod) to be
Thu, 05 Jan 2006 12:09:26 +0100 urbanc changed the name of the type "nOption" to "noption".
less more (0) -60 tip