--- a/src/HOL/RealDef.thy Mon Nov 29 13:44:54 2010 +0100
+++ b/src/HOL/RealDef.thy Mon Nov 29 22:32:06 2010 +0100
@@ -358,7 +358,7 @@
apply (simp add: quotientI X)
apply (rule the_equality)
apply clarsimp
- apply (erule congruent.congruent [OF f])
+ apply (erule congruentD [OF f])
apply (erule bspec)
apply simp
apply (rule refl_onD [OF refl_realrel])
@@ -370,7 +370,7 @@
assumes X: "cauchy X" and Y: "cauchy Y"
shows "real_case (\<lambda>X. real_case (\<lambda>Y. f X Y) (Real Y)) (Real X) = f X Y"
apply (subst real_case_1 [OF _ X])
- apply (rule congruent.intro)
+ apply (rule congruentI)
apply (subst real_case_1 [OF _ Y])
apply (rule congruent2_implies_congruent [OF equiv_realrel f])
apply (simp add: realrel_def)
@@ -416,7 +416,7 @@
lemma minus_respects_realrel:
"(\<lambda>X. Real (\<lambda>n. - X n)) respects realrel"
-proof (rule congruent.intro)
+proof (rule congruentI)
fix X Y assume "(X, Y) \<in> realrel"
hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
unfolding realrel_def by simp_all
@@ -492,7 +492,7 @@
lemma inverse_respects_realrel:
"(\<lambda>X. if vanishes X then c else Real (\<lambda>n. inverse (X n))) respects realrel"
(is "?inv respects realrel")
-proof (rule congruent.intro)
+proof (rule congruentI)
fix X Y assume "(X, Y) \<in> realrel"
hence X: "cauchy X" and Y: "cauchy Y" and XY: "vanishes (\<lambda>n. X n - Y n)"
unfolding realrel_def by simp_all
@@ -622,7 +622,7 @@
assumes sym: "sym r"
assumes P: "\<And>x y. (x, y) \<in> r \<Longrightarrow> P x \<Longrightarrow> P y"
shows "P respects r"
-apply (rule congruent.intro)
+apply (rule congruentI)
apply (rule iffI)
apply (erule (1) P)
apply (erule (1) P [OF symD [OF sym]])