# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259459502 -3600
# Node ID b5e7e73bf31d62cdec89737e5c3af0d0e113b3df
# Parent  24fa145fc2e325c61090a273659dd5390c9d63c5
tuned

diff -r 24fa145fc2e3 -r b5e7e73bf31d QuotMain.thy
--- a/QuotMain.thy	Sat Nov 28 19:14:12 2009 +0100
+++ b/QuotMain.thy	Sun Nov 29 02:51:42 2009 +0100
@@ -894,8 +894,8 @@
 ML {*
 fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [
-    (* "cong" rule of the of the relation *)
-    (* a \<approx> b = c \<approx> d ----> \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> *)
+    (* "cong" rule of the of the relation / transitivity*)
+    (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
     NDT ctxt "1" (resolve_tac trans2),
 
     (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
@@ -914,7 +914,7 @@
     NDT ctxt "6" (bex_rsp_tac ctxt),
 
     (* respectfulness of constants *)
-    NDT ctxt "7" (resolve_tac rsp_thms),
+    DT ctxt "7" (resolve_tac rsp_thms),
 
     (* reflexivity of operators arising from Cong_tac *)
     NDT ctxt "8" (rtac @{thm refl}),
@@ -924,11 +924,11 @@
     NDT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 
                   THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
 
-    (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> APPLY_RSP   provided type of t needs lifting *)
+    (* R (t $ \<dots>) (t' $ \<dots>) ----> APPLY_RSP   provided type of t needs lifting *)
     NDT ctxt "A" ((APPLY_RSP_TAC rty ctxt THEN' 
                 (RANGE [SOLVES' (quotient_tac quot_thms), SOLVES' (quotient_tac quot_thms)]))),
 
-    (* (op =) (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong   provided type of t does not need lifting *)
+    (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)
     (* merge with previous tactic *)
     NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
 
@@ -936,6 +936,7 @@
     NDT ctxt "C" (rtac @{thm ext}),
     
     (* reflexivity of the basic relations *)
+    (* R \<dots> \<dots> *)
     NDT ctxt "D" (resolve_tac rel_refl),
 
     (* resolving with R x y assumptions *)