diff -r 1e08743b6997 -r a9e55e1ef64c Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Fri Dec 11 16:32:40 2009 +0100
+++ b/Quot/QuotMain.thy	Fri Dec 11 17:19:38 2009 +0100
@@ -17,14 +17,14 @@
 begin
 
 definition
-  ABS::"'a \<Rightarrow> 'b"
+  abs::"'a \<Rightarrow> 'b"
 where
-  "ABS x \<equiv> Abs (R x)"
+  "abs x \<equiv> Abs (R x)"
 
 definition
-  REP::"'b \<Rightarrow> 'a"
+  rep::"'b \<Rightarrow> 'a"
 where
-  "REP a = Eps (Rep a)"
+  "rep a = Eps (Rep a)"
 
 lemma lem9:
   shows "R (Eps (R x)) = R x"
@@ -36,9 +36,9 @@
 qed
 
 theorem thm10:
-  shows "ABS (REP a) \<equiv> a"
+  shows "abs (rep a) \<equiv> a"
   apply  (rule eq_reflection)
-  unfolding ABS_def REP_def
+  unfolding abs_def rep_def
 proof -
   from rep_prop
   obtain x where eq: "Rep a = R x" by auto
@@ -50,9 +50,9 @@
   show "Abs (R (Eps (Rep a))) = a" by simp
 qed
 
-lemma REP_refl:
-  shows "R (REP a) (REP a)"
-unfolding REP_def
+lemma rep_refl:
+  shows "R (rep a) (rep a)"
+unfolding rep_def
 by (simp add: equivp[simplified equivp_def])
 
 lemma lem7:
@@ -64,21 +64,21 @@
 done
 
 theorem thm11:
-  shows "R r r' = (ABS r = ABS r')"
-unfolding ABS_def
+  shows "R r r' = (abs r = abs r')"
+unfolding abs_def
 by (simp only: equivp[simplified equivp_def] lem7)
 
 
-lemma REP_ABS_rsp:
-  shows "R f (REP (ABS g)) = R f g"
-  and   "R (REP (ABS g)) f = R g f"
+lemma rep_abs_rsp:
+  shows "R f (rep (abs g)) = R f g"
+  and   "R (rep (abs g)) f = R g f"
 by (simp_all add: thm10 thm11)
 
 lemma Quotient:
-  "Quotient R ABS REP"
+  "Quotient R abs rep"
 apply(unfold Quotient_def)
 apply(simp add: thm10)
-apply(simp add: REP_refl)
+apply(simp add: rep_refl)
 apply(subst thm11[symmetric])
 apply(simp add: equivp[simplified equivp_def])
 done