# HG changeset patch
# User haftmann
# Date 1291034694 -3600
# Node ID 6e2d17cc0d1defd386e563fe4f08e81df80ea043
# Parent  fa64f627856824ef83d3f2c0b258e8cd15b056c9
equivI has replaced equiv.intro

diff -r fa64f6278568 -r 6e2d17cc0d1d NEWS
--- a/NEWS	Mon Nov 29 12:15:14 2010 +0100
+++ b/NEWS	Mon Nov 29 13:44:54 2010 +0100
@@ -89,6 +89,9 @@
 
 *** HOL ***
 
+* Abandoned locale equiv for equivalence relations.  INCOMPATIBILITY: use
+equivI rather than equiv_intro.
+
 * Code generator: globbing constant expressions "*" and "Theory.*" have been
 replaced by the more idiomatic "_" and "Theory._".  INCOMPATIBILITY.
 
diff -r fa64f6278568 -r 6e2d17cc0d1d src/HOL/Algebra/Coset.thy
--- a/src/HOL/Algebra/Coset.thy	Mon Nov 29 12:15:14 2010 +0100
+++ b/src/HOL/Algebra/Coset.thy	Mon Nov 29 13:44:54 2010 +0100
@@ -606,7 +606,7 @@
 proof -
   interpret group G by fact
   show ?thesis
-  proof (intro equiv.intro)
+  proof (intro equivI)
     show "refl_on (carrier G) (rcong H)"
       by (auto simp add: r_congruent_def refl_on_def) 
   next
diff -r fa64f6278568 -r 6e2d17cc0d1d src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Mon Nov 29 12:15:14 2010 +0100
+++ b/src/HOL/Equiv_Relations.thy	Mon Nov 29 13:44:54 2010 +0100
@@ -13,6 +13,15 @@
 definition equiv :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" where
   "equiv A r \<longleftrightarrow> refl_on A r \<and> sym r \<and> trans r"
 
+lemma equivI:
+  "refl_on A r \<Longrightarrow> sym r \<Longrightarrow> trans r \<Longrightarrow> equiv A r"
+  by (simp add: equiv_def)
+
+lemma equivE:
+  assumes "equiv A r"
+  obtains "refl_on A r" and "sym r" and "trans r"
+  using assms by (simp add: equiv_def)
+
 text {*
   Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\<inverse> O
   r = r"}.
diff -r fa64f6278568 -r 6e2d17cc0d1d src/HOL/Library/Fraction_Field.thy
--- a/src/HOL/Library/Fraction_Field.thy	Mon Nov 29 12:15:14 2010 +0100
+++ b/src/HOL/Library/Fraction_Field.thy	Mon Nov 29 13:44:54 2010 +0100
@@ -43,7 +43,7 @@
 qed
   
 lemma equiv_fractrel: "equiv {x. snd x \<noteq> 0} fractrel"
-  by (rule equiv.intro [OF refl_fractrel sym_fractrel trans_fractrel])
+  by (rule equivI [OF refl_fractrel sym_fractrel trans_fractrel])
 
 lemmas UN_fractrel = UN_equiv_class [OF equiv_fractrel]
 lemmas UN_fractrel2 = UN_equiv_class2 [OF equiv_fractrel equiv_fractrel]
diff -r fa64f6278568 -r 6e2d17cc0d1d src/HOL/NSA/StarDef.thy
--- a/src/HOL/NSA/StarDef.thy	Mon Nov 29 12:15:14 2010 +0100
+++ b/src/HOL/NSA/StarDef.thy	Mon Nov 29 13:44:54 2010 +0100
@@ -62,7 +62,7 @@
 by (simp add: starrel_def)
 
 lemma equiv_starrel: "equiv UNIV starrel"
-proof (rule equiv.intro)
+proof (rule equivI)
   show "refl starrel" by (simp add: refl_on_def)
   show "sym starrel" by (simp add: sym_def eq_commute)
   show "trans starrel" by (auto intro: transI elim!: ultra)
diff -r fa64f6278568 -r 6e2d17cc0d1d src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Mon Nov 29 12:15:14 2010 +0100
+++ b/src/HOL/Rat.thy	Mon Nov 29 13:44:54 2010 +0100
@@ -44,7 +44,7 @@
 qed
   
 lemma equiv_ratrel: "equiv {x. snd x \<noteq> 0} ratrel"
-  by (rule equiv.intro [OF refl_on_ratrel sym_ratrel trans_ratrel])
+  by (rule equivI [OF refl_on_ratrel sym_ratrel trans_ratrel])
 
 lemmas UN_ratrel = UN_equiv_class [OF equiv_ratrel]
 lemmas UN_ratrel2 = UN_equiv_class2 [OF equiv_ratrel equiv_ratrel]
diff -r fa64f6278568 -r 6e2d17cc0d1d src/HOL/RealDef.thy
--- a/src/HOL/RealDef.thy	Mon Nov 29 12:15:14 2010 +0100
+++ b/src/HOL/RealDef.thy	Mon Nov 29 13:44:54 2010 +0100
@@ -324,7 +324,7 @@
 
 lemma equiv_realrel: "equiv {X. cauchy X} realrel"
   using refl_realrel sym_realrel trans_realrel
-  by (rule equiv.intro)
+  by (rule equivI)
 
 subsection {* The field of real numbers *}