# HG changeset patch
# User berghofe
# Date 1189699688 -7200
# Node ID c80e1871098b64a6393716d209954c7534846ab9
# Parent  9a4cce088aec260372545b05412772e8cbd8e469
Added equivariance lemmas for induct_forall.

diff -r 9a4cce088aec -r c80e1871098b src/HOL/Nominal/nominal_atoms.ML
--- a/src/HOL/Nominal/nominal_atoms.ML	Thu Sep 13 18:06:50 2007 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Sep 13 18:08:08 2007 +0200
@@ -21,6 +21,8 @@
 val finite_emptyI = @{thm "finite.emptyI"};
 val Collect_const = @{thm "Collect_const"};
 
+val inductive_forall_def = @{thm "induct_forall_def"};
+
 
 (* theory data *)
 
@@ -803,7 +805,13 @@
             ||>> PureThy.add_thmss [(("supp_atm", (inst_at [at_supp]) @ (inst_dj [dj_supp])),[])]
             ||>> PureThy.add_thmss [(("exists_fresh", inst_at [at_exists_fresh]),[])]
             ||>> PureThy.add_thmss [(("exists_fresh'", inst_at [at_exists_fresh']),[])]
-            ||>> PureThy.add_thmss [(("all_eqvt", inst_pt_at [all_eqvt]),[NominalThmDecls.eqvt_force_add])] 
+            ||>> PureThy.add_thmss
+              let
+                val thms1 = inst_pt_at [all_eqvt];
+                val thms2 = map (fold_rule [inductive_forall_def]) thms1
+              in
+                [(("all_eqvt", thms1 @ thms2), [NominalThmDecls.eqvt_force_add])]
+              end
             ||>> PureThy.add_thmss [(("ex_eqvt", inst_pt_at [ex_eqvt]),[NominalThmDecls.eqvt_force_add])]
             ||>> PureThy.add_thmss 
 	      let val thms1 = inst_at [at_fresh]