--- a/QuotScript.thy	Mon Oct 26 10:02:50 2009 +0100
+++ b/QuotScript.thy	Mon Oct 26 10:20:20 2009 +0100
@@ -486,16 +486,7 @@
   apply (simp add: FUN_REL.simps Bex_def IN_RESPECTS)
   done
 
-(* TODO: 
-- [FORALL_PRS, EXISTS_PRS, COND_PRS];
-> val it =
-    [|- !R abs rep.
-          QUOTIENT R abs rep ==>
-          !f. $! f <=> RES_FORALL (respects R) ((abs --> I) f),
-     |- !R abs rep.
-          QUOTIENT R abs rep ==>
-          !f. $? f <=> RES_EXISTS (respects R) ((abs --> I) f),
-*)
+
 lemma FORALL_PRS:
   assumes a: "QUOTIENT R absf repf"
   shows "All f = Ball (Respects R) ((absf ---> id) f)"
@@ -513,9 +504,7 @@
 lemma COND_PRS:
   assumes a: "QUOTIENT R absf repf"
   shows "(if a then b else c) = absf (if a then repf b else repf c)"
-  using a
-  unfolding QUOTIENT_def
-  sorry
+  using a unfolding QUOTIENT_def by auto
 
 (* These are the fixed versions, general ones need to be proved. *)
 lemma ho_all_prs: