src/HOL/Nominal/Examples/Weakening.thy
Fri, 18 Aug 2017 20:47:47 +0200 wenzelm session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
Thu, 26 May 2016 17:51:22 +0200 wenzelm isabelle update_cartouches -c -t;
Tue, 23 Feb 2016 16:25:08 +0100 nipkow more canonical names
Sat, 17 Oct 2009 14:43:18 +0200 wenzelm eliminated hard tabulators, guessing at each author's individual tab-width;
Thu, 22 May 2008 16:34:41 +0200 urbanc made the naming of the induction principles consistent: weak_induct is
Wed, 12 Mar 2008 11:57:12 +0100 urbanc tuned
Mon, 11 Feb 2008 15:19:17 +0100 urbanc tuned proofs and comments
Tue, 01 Jan 2008 07:28:20 +0100 urbanc tuned proofs and comments
Thu, 20 Dec 2007 01:07:21 +0100 urbanc polishing of some proofs
Sun, 21 Oct 2007 19:12:05 +0200 urbanc further comments
Sun, 21 Oct 2007 19:04:53 +0200 urbanc polished the proofs and added a version of the weakening lemma that does not use the variable convention
Sun, 12 Aug 2007 18:53:03 +0200 wenzelm added type constraints to resolve syntax ambiguities;
Wed, 11 Jul 2007 11:36:06 +0200 berghofe Renamed inductive2 to inductive.
Thu, 19 Apr 2007 16:38:59 +0200 berghofe nominal_inductive no longer proves equivariance.
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
Tue, 27 Mar 2007 18:28:22 +0200 urbanc adapted to new nominal_inductive infrastructure
Tue, 06 Mar 2007 15:28:22 +0100 urbanc major update of the nominal package; there is now an infrastructure
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
Thu, 23 Nov 2006 17:52:48 +0100 urbanc fixed some typos
Thu, 23 Nov 2006 14:11:49 +0100 urbanc tuned the proof of the strong induction principle
Fri, 17 Nov 2006 17:32:30 +0100 urbanc added an intro lemma for freshness of products; set up
Fri, 17 Nov 2006 02:20:03 +0100 wenzelm more robust syntax for definition/abbreviation/notation;
Wed, 15 Nov 2006 16:23:55 +0100 urbanc replaced exists_fresh lemma with a version formulated with obtains;
Tue, 14 Nov 2006 22:16:54 +0100 wenzelm inductive2: canonical specification syntax;
Mon, 30 Oct 2006 13:07:51 +0100 urbanc new file for defining functions in the lambda-calculus
Wed, 18 Oct 2006 23:06:51 +0200 urbanc adapted to Stefan's new inductive package and cleaning up
Tue, 10 Oct 2006 16:26:59 +0200 urbanc made some proof look more like the ones in Barendregt
Mon, 11 Sep 2006 21:35:19 +0200 wenzelm induct method: renamed 'fixing' to 'arbitrary';
Sun, 02 Jul 2006 17:27:10 +0200 urbanc added more infrastructure for the recursion combinator
Fri, 28 Apr 2006 15:58:30 +0200 berghofe Capitalized theory names.
Wed, 11 Jan 2006 17:07:57 +0100 urbanc tuned proofs
Wed, 11 Jan 2006 14:00:11 +0100 urbanc tuned the eqvt-proof
Mon, 05 Dec 2005 17:02:20 +0100 urbanc tuned
Mon, 05 Dec 2005 10:33:30 +0100 urbanc tuned
Sun, 04 Dec 2005 12:14:40 +0100 urbanc tuned
Thu, 01 Dec 2005 04:46:17 +0100 urbanc changed "fresh:" to "avoiding:" and cleaned up the weakening example
Wed, 30 Nov 2005 14:27:09 +0100 urbanc adapted to the new nominal_induction
Mon, 28 Nov 2005 05:03:00 +0100 urbanc some small tuning
Mon, 07 Nov 2005 15:12:13 +0100 urbanc Initial commit of the theory "Weakening".
less more (0) tip