# HG changeset patch
# User berghofe
# Date 1189699610 -7200
# Node ID 9a4cce088aec260372545b05412772e8cbd8e469
# Parent  4970fb01aa017e839b59209be8d37f087c95fda1
Added equivariance lemma for induct_implies.

diff -r 4970fb01aa01 -r 9a4cce088aec src/HOL/Nominal/Nominal.thy
--- a/src/HOL/Nominal/Nominal.thy	Tue Sep 11 14:26:49 2007 +0200
+++ b/src/HOL/Nominal/Nominal.thy	Thu Sep 13 18:06:50 2007 +0200
@@ -3233,6 +3233,7 @@
   (* connectives *)
   if_eqvt imp_eqvt disj_eqvt conj_eqvt neg_eqvt 
   true_eqvt false_eqvt
+  imp_eqvt [folded induct_implies_def]
   
   (* datatypes *)
   perm_unit.simps