src/HOL/Nominal/Nominal.thy
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Thu, 15 Mar 2012 22:08:53 +0100 wenzelm declare command keywords via theory header, including strict checking outside Pure;
Thu, 15 Mar 2012 19:02:34 +0100 wenzelm declare minor keywords via theory header;
Tue, 10 Jan 2012 23:49:53 +0100 berghofe Reverted several lemmas involving sets to the state before the
Sat, 24 Dec 2011 15:53:08 +0100 haftmann treatment of type constructor `set`
Wed, 30 Nov 2011 16:27:10 +0100 wenzelm prefer typedef without extra definition and alternative name;
Thu, 24 Nov 2011 21:01:06 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Thu, 08 Sep 2011 00:35:22 +0200 haftmann merged
Tue, 06 Sep 2011 22:04:14 +0200 haftmann merged
Mon, 05 Sep 2011 22:02:32 +0200 haftmann tuned
Sun, 04 Sep 2011 08:43:06 +0200 haftmann pseudo-definition for perms on sets; tuned
Sat, 03 Sep 2011 23:59:36 +0200 haftmann tuned specifications
Sat, 03 Sep 2011 17:32:34 +0200 haftmann tuned specifications and proofs
Sun, 28 Aug 2011 14:16:14 +0200 haftmann tuned
Mon, 21 Feb 2011 17:43:23 +0100 wenzelm modernized specifications;
Sat, 15 Jan 2011 12:38:56 +0100 berghofe Finally removed old primrec package, since Primrec.add_primrec_global
Fri, 14 Jan 2011 15:44:47 +0100 wenzelm eliminated global prems;
Wed, 29 Dec 2010 17:34:41 +0100 wenzelm explicit file specifications -- avoid secondary load path;
Wed, 29 Sep 2010 09:07:58 +0200 haftmann moved old_primrec source to nominal package, where it is still used
Mon, 13 Sep 2010 11:13:15 +0200 nipkow renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
Tue, 07 Sep 2010 10:05:19 +0200 nipkow expand_fun_eq -> ext_iff
Mon, 01 Mar 2010 13:42:31 +0100 haftmann merged
Mon, 01 Mar 2010 13:40:23 +0100 haftmann replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
Wed, 24 Feb 2010 21:59:21 +0100 wenzelm proper type syntax (cf. 7425aece4ee3);
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Mon, 21 Sep 2009 15:02:23 +0200 Christian Urban tuned some proofs
Fri, 03 Jul 2009 16:51:08 +0200 haftmann nominal.ML is nominal_datatype.ML
Fri, 19 Jun 2009 17:23:21 +0200 haftmann discontinued ancient tradition to suffix certain ML module names with "_package"
Sun, 26 Apr 2009 23:16:24 +0200 Christian Urban reorganised the section about fresh_star and added lemma pt_fresh_star_pi
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)
Wed, 04 Mar 2009 11:05:29 +0100 blanchet Merge.
Wed, 04 Mar 2009 10:45:52 +0100 blanchet Merge.
Thu, 26 Feb 2009 16:34:03 +0100 berghofe Added postprocessing rules for fresh_star.
Wed, 25 Feb 2009 19:34:00 +0100 berghofe Added lemmas for normalizing freshness results involving fresh_star.
Wed, 25 Feb 2009 11:02:25 +0100 berghofe Added equivariance lemmas for fresh_star.
Sat, 14 Feb 2009 08:45:16 +0100 nipkow more finiteness changes
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
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code
Tue, 21 Oct 2008 21:18:54 +0200 berghofe Added nominal_inductive2.ML
Fri, 26 Sep 2008 14:51:27 +0200 berghofe Added some more lemmas that are useful in proof of strong induction rule.
Mon, 22 Sep 2008 19:46:24 +0200 urbanc made the perm_simp tactic to understand options such as (no_asm)
Wed, 27 Aug 2008 04:47:30 +0200 urbanc added equivariance lemmas for ex1 and the
Sun, 27 Jul 2008 20:08:16 +0200 urbanc simplified a proof
Fri, 27 Jun 2008 00:37:30 +0200 urbanc added a lemma to at_swap_simps
Mon, 16 Jun 2008 17:54:39 +0200 wenzelm allE_Nil: only one copy, proven in regular theory source;
Thu, 08 May 2008 04:20:08 +0200 urbanc added at_set_avoiding lemmas
Wed, 07 May 2008 10:57:19 +0200 berghofe Adapted to encoding of sets as predicates
Fri, 02 May 2008 22:43:14 +0200 urbanc added more infrastructure for fresh_star
Fri, 02 May 2008 16:32:51 +0200 urbanc polished the proof for atm_prm_fresh and more lemmas for fresh_star
Thu, 03 Apr 2008 11:48:48 +0200 urbanc added generalised definitions for freshness of sets of atoms
Wed, 19 Mar 2008 22:50:42 +0100 wenzelm more antiquotations;
Mon, 18 Feb 2008 03:12:08 +0100 urbanc added eqvt-flag to subseteq-lemma
Thu, 24 Jan 2008 11:23:11 +0100 berghofe Added lemma at_fin_set_fresh.
Fri, 14 Sep 2007 13:32:07 +0200 urbanc reverted back to the old version of the equivariance lemma for ALL
Thu, 13 Sep 2007 23:58:38 +0200 urbanc some cleaning up to do with contexts
Thu, 13 Sep 2007 18:06:50 +0200 berghofe Added equivariance lemma for induct_implies.
Thu, 06 Sep 2007 16:28:42 +0200 urbanc trivial cleaning up
Wed, 11 Jul 2007 11:28:13 +0200 berghofe Adapted to new inductive definition package.
Thu, 14 Jun 2007 23:04:36 +0200 wenzelm tuned proofs: avoid implicit prems;
Thu, 31 May 2007 15:23:35 +0200 urbanc tuned the proof
less more (0) -100 -60 tip