diff -r 03671ff78226 -r 75af61f32ece QuotMain.thy
--- a/QuotMain.thy	Sat Nov 28 14:03:01 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 14:15:05 2009 +0100
@@ -248,6 +248,8 @@
 end
 
 fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))]
+
+fun NDT ctxt s tac = tac
 *}
 
 section {*  Infrastructure about definitions *}
@@ -833,8 +835,7 @@
   Subgoal.FOCUS (fn {concl, ...} =>
      case (term_of concl) of
         (_ $ (_ $ (Const (@{const_name Ball}, _) $ _) 
-                $ (Const (@{const_name Ball}, _) $ _))) =>
-            rtac @{thm FUN_REL_I} 1
+                $ (Const (@{const_name Ball}, _) $ _))) => rtac @{thm FUN_REL_I} 1
       |_ => no_tac)
 *}
 
@@ -843,8 +844,7 @@
   Subgoal.FOCUS (fn {concl, context = ctxt, ...} =>
      case (term_of concl) of
         (_ $ (_ $ (Const (@{const_name Bex}, _) $ _) 
-                $ (Const (@{const_name Bex}, _) $ _))) =>
-            rtac @{thm FUN_REL_I} 1
+                $ (Const (@{const_name Bex}, _) $ _))) => rtac @{thm FUN_REL_I} 1
       | _ => no_tac)
 *}
 
@@ -965,7 +965,8 @@
     DT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' 
                 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
 
-    (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *)
+    (* (op =) (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong   provided type of t does not need lifting *)
+    (* merge with previous tactic *)
     DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
 
     (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)