--- a/Derivatives.thy	Thu Jul 28 17:52:36 2011 +0000
+++ b/Derivatives.thy	Sun Jul 31 10:27:41 2011 +0000
@@ -417,7 +417,7 @@
 
 lemma MN_Rel_Ders:
   shows "x \<approx>A y \<longleftrightarrow> Ders x A = Ders y A"
-unfolding Ders_def str_eq_def str_eq_rel_def
+unfolding Ders_def str_eq_def
 by auto
 
 subsection {*
@@ -442,20 +442,17 @@
   qed
   moreover 
   have "=(\<lambda>x. pders x r)= \<subseteq> \<approx>(lang r)"
-    unfolding tag_eq_rel_def
-    unfolding str_eq_def2
-    unfolding MN_Rel_Ders
-    unfolding Ders_pders
-    by auto
+    unfolding tag_eq_def
+    by (auto simp add: MN_Rel_Ders Ders_pders)
   moreover 
   have "equiv UNIV =(\<lambda>x. pders x r)="
     unfolding equiv_def refl_on_def sym_def trans_def
-    unfolding tag_eq_rel_def
+    unfolding tag_eq_def
     by auto
   moreover
   have "equiv UNIV (\<approx>(lang r))"
     unfolding equiv_def refl_on_def sym_def trans_def
-    unfolding str_eq_rel_def
+    unfolding str_eq_def
     by auto
   ultimately show "finite (UNIV // \<approx>(lang r))" 
     by (rule refined_partition_finite)