# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1265196718 -3600
# Node ID 0d832c36b1bbd810503783a0505c28536fa2323f
# Parent  6911934c98c737b4dd89fc0182be8ea43b0ece22
fixed proofs in Abs.thy

diff -r 6911934c98c7 -r 0d832c36b1bb Quot/Nominal/Abs.thy
--- a/Quot/Nominal/Abs.thy	Wed Feb 03 12:13:22 2010 +0100
+++ b/Quot/Nominal/Abs.thy	Wed Feb 03 12:31:58 2010 +0100
@@ -133,17 +133,18 @@
   assumes a: "\<And>x. pi \<bullet> (f x) = f (pi \<bullet> x)"
   and     b: "\<exists>pia. ({atom a}, t) \<approx>gen (\<lambda>x1 x2. R x1 x2 \<and> R (pi \<bullet> x1) (pi \<bullet> x2)) f pia ({atom b}, s)"
   shows  "\<exists>pia. ({atom (pi \<bullet> a)}, pi \<bullet> t) \<approx>gen R f pia ({atom (pi \<bullet> b)}, pi \<bullet> s)"
-  using b apply -
+  using b 
+  apply -
   apply(erule exE)
   apply(rule_tac x="pi \<bullet> pia" in exI)
   apply(simp add: alpha_gen.simps)
   apply(erule conjE)+
   apply(rule conjI)
   apply(rule_tac ?p1="- pi" in permute_eq_iff[THEN iffD1])
-  apply(simp add: a[symmetric] atom_eqvt eqvts)
+  apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt)
   apply(rule conjI)
   apply(rule_tac ?p1="- pi" in fresh_star_permute_iff[THEN iffD1])
-  apply(simp add: a[symmetric] eqvts atom_eqvt)
+  apply(simp add: a[symmetric] atom_eqvt Diff_eqvt insert_eqvt set_eqvt empty_eqvt)
   apply(subst permute_eqvt[symmetric])
   apply(simp)
   done
diff -r 6911934c98c7 -r 0d832c36b1bb Quot/Nominal/Nominal2_Eqvt.thy
--- a/Quot/Nominal/Nominal2_Eqvt.thy	Wed Feb 03 12:13:22 2010 +0100
+++ b/Quot/Nominal/Nominal2_Eqvt.thy	Wed Feb 03 12:31:58 2010 +0100
@@ -244,7 +244,7 @@
 
 declare permute_pure [eqvt]
 
-thm eqvt
+(* thm eqvts *)
 
 text {* helper lemmas for the eqvt_tac *}
 
diff -r 6911934c98c7 -r 0d832c36b1bb Quot/Nominal/Terms.thy
--- a/Quot/Nominal/Terms.thy	Wed Feb 03 12:13:22 2010 +0100
+++ b/Quot/Nominal/Terms.thy	Wed Feb 03 12:31:58 2010 +0100
@@ -646,13 +646,7 @@
 quotient_type 
   qtrm4 = trm4 / alpha4 and
   qtrm4list = "trm4 list" / alpha4list
-  by (simp_all add: alpha4_equivp alpha4list_equivp)
-
-
-
-
-
-
+  by (simp_all add: alpha4_equivp alpha4list_equivp
 
 
 datatype rtrm5 =
diff -r 6911934c98c7 -r 0d832c36b1bb Quot/Nominal/nominal_thmdecls.ML
--- a/Quot/Nominal/nominal_thmdecls.ML	Wed Feb 03 12:13:22 2010 +0100
+++ b/Quot/Nominal/nominal_thmdecls.ML	Wed Feb 03 12:31:58 2010 +0100
@@ -113,7 +113,7 @@
   Attrib.setup @{binding "eqvt_force"} (Attrib.add_del eqvt_force_add eqvt_force_del) 
     (cat_lines ["declaration of equivariance lemmas - they will will be", 
                 "added/deleted directly to the eqvt thm-list"]) #>
-  PureThy.add_thms_dynamic (@{binding "eqvt"}, content);
+  PureThy.add_thms_dynamic (@{binding "eqvts"}, content);
 
 
 end;