src/HOL/Nominal/Examples/CR.thy
Thu, 14 Jun 2007 23:04:36 +0200 wenzelm tuned proofs: avoid implicit prems;
Fri, 27 Apr 2007 18:50:27 +0200 urbanc tuned some proofs in CR and properly included CR_Takahashi
Thu, 19 Apr 2007 16:38:59 +0200 berghofe nominal_inductive no longer proves equivariance.
Wed, 28 Mar 2007 19:16:11 +0200 berghofe - Renamed <predicate>_eqvt to <predicate>.eqvt
Wed, 28 Mar 2007 17:27:44 +0200 urbanc adapted to new nominal_inductive
Mon, 27 Nov 2006 14:05:43 +0100 urbanc adapted function definitions to new syntax
Wed, 15 Nov 2006 16:23:55 +0100 urbanc replaced exists_fresh lemma with a version formulated with obtains;
less more (0) -10 -7 tip