--- a/Quot/Quotient.thy	Fri Feb 12 12:06:09 2010 +0100
+++ b/Quot/Quotient.thy	Fri Feb 12 15:06:20 2010 +0100
@@ -12,22 +12,23 @@
   ("quotient_tacs.ML")
 begin
 
+
 text {*
   Basic definition for equivalence relations
   that are represented by predicates.
 *}
 
 definition
-  "equivp E \<longleftrightarrow> (\<forall>x y. E x y = (E x = E y))"
+  "equivp E \<equiv> \<forall>x y. E x y = (E x = E y)"
 
 definition
-  "reflp E \<longleftrightarrow> (\<forall>x. E x x)"
+  "reflp E \<equiv> \<forall>x. E x x"
 
 definition
-  "symp E \<longleftrightarrow> (\<forall>x y. E x y \<longrightarrow> E y x)"
+  "symp E \<equiv> \<forall>x y. E x y \<longrightarrow> E y x"
 
 definition
-  "transp E \<longleftrightarrow> (\<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z)"
+  "transp E \<equiv> \<forall>x y z. E x y \<and> E y z \<longrightarrow> E x z"
 
 lemma equivp_reflp_symp_transp:
   shows "equivp E = (reflp E \<and> symp E \<and> transp E)"
@@ -51,19 +52,15 @@
   shows "equivp R"
   using assms by (simp add: equivp_reflp_symp_transp)
 
-lemma eq_imp_rel:
-  shows "equivp R \<Longrightarrow> a = b \<longrightarrow> R a b"
-  by (simp add: equivp_reflp)
-
 lemma identity_equivp:
   shows "equivp (op =)"
   unfolding equivp_def
   by auto
 
+text {* Partial equivalences: not yet used anywhere *}
 
-text {* Partial equivalences: not yet used anywhere *}
 definition
-  "part_equivp E \<longleftrightarrow> ((\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y))))"
+  "part_equivp E \<equiv> (\<exists>x. E x x) \<and> (\<forall>x y. E x y = (E x x \<and> E y y \<and> (E x = E y)))"
 
 lemma equivp_implies_part_equivp:
   assumes a: "equivp E"
@@ -88,7 +85,7 @@
 definition
   Respects
 where
-  "Respects R x \<longleftrightarrow> (R x x)"
+  "Respects R x \<equiv> R x x"
 
 lemma in_respects:
   shows "(x \<in> Respects R) = R x x"
@@ -130,7 +127,7 @@
 section {* Quotient Predicate *}
 
 definition
-  "Quotient E Abs Rep \<longleftrightarrow>
+  "Quotient E Abs Rep \<equiv>
      (\<forall>a. Abs (Rep a) = a) \<and> (\<forall>a. E (Rep a) (Rep a)) \<and>
      (\<forall>r s. E r s = (E r r \<and> E s s \<and> (Abs r = Abs s)))"
 
@@ -354,6 +351,7 @@
   apply(simp add: reflp_def)
   done
 
+(* Next four lemmas are unused *)
 lemma all_reg:
   assumes a: "!x :: 'a. (P x --> Q x)"
   and     b: "All P"
@@ -378,6 +376,7 @@
   shows "Bex R Q"
   using a b by (metis COMBC_def Collect_def Collect_mem_eq)
 
+
 lemma ball_all_comm:
   assumes "\<And>y. (\<forall>x\<in>P. A x y) \<longrightarrow> (\<forall>x. B x y)"
   shows "(\<forall>x\<in>P. \<forall>y. A x y) \<longrightarrow> (\<forall>x. \<forall>y. B x y)"