# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259413381 -3600
# Node ID 03671ff78226adcb48e9230bd719edf387dfdf7b
# Parent  7beed9b75ea28e7fe1cb5e601a6339c6fd463d08
tuned comments

diff -r 7beed9b75ea2 -r 03671ff78226 QuotMain.thy
--- a/QuotMain.thy	Sat Nov 28 13:54:48 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 14:03:01 2009 +0100
@@ -931,23 +931,23 @@
   (FIRST' [
     (K (print_tac "start")) THEN' (K no_tac), 
   
-    (* "cong" rule of the of the relation    *)
-    (* \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> \<Longrightarrow> a \<approx> b = c \<approx> d *)
+    (* "cong" rule of the of the relation *)
+    (* a \<approx> b = c \<approx> d ----> \<lbrakk>a \<approx> c; b \<approx> d\<rbrakk> *)
     DT ctxt "1" (resolve_tac trans2),
 
-    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
+    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
     DT ctxt "2" (lambda_res_tac ctxt),
 
-    (* = (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *)
+    (* (op =) (Ball\<dots>) (Ball\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
     DT ctxt "3" (rtac @{thm RES_FORALL_RSP}),
 
-    (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
+    (* (R1 ===> R2) (Ball\<dots>) (Ball\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Ball\<dots>x) (Ball\<dots>y) *)
     DT ctxt "4" (ball_rsp_tac ctxt),
 
-    (* = (Bex\<dots>) (Bex\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *)
+    (* (op =) (Bex\<dots>) (Bex\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
     DT ctxt "5" (rtac @{thm RES_EXISTS_RSP}),
 
-    (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) \<Longrightarrow> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
+    (* (R1 ===> R2) (Bex\<dots>) (Bex\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (Bex\<dots>x) (Bex\<dots>y) *)
     DT ctxt "6" (bex_rsp_tac ctxt),
 
     (* respectfulness of constants *)
@@ -956,7 +956,7 @@
     (* reflexivity of operators arising from Cong_tac *)
     DT ctxt "8" (rtac @{thm refl}),
 
-    (* R (\<dots>) (Rep (Abs \<dots>)) \<Longrightarrow> R (\<dots>) (\<dots>) *)
+    (* R (\<dots>) (Rep (Abs \<dots>)) ----> R (\<dots>) (\<dots>) *)
     (* observe ---> *) 
     DT ctxt "9" ((instantiate_tac @{thm REP_ABS_RSP(1)} ctxt 
                   THEN' (RANGE [SOLVES' (quotient_tac quot_thms)]))),
@@ -968,7 +968,7 @@
     (* R (t $ \<dots>) (t' $ \<dots>) \<Longrightarrow> Cong provided R = (op =) and t does not need lifting *)
     DT ctxt "B" (Cong_Tac.cong_tac @{thm cong}),
 
-    (* = (\<lambda>x\<dots>) (\<lambda>x\<dots>) \<Longrightarrow> = (\<dots>) (\<dots>) *)
+    (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
     DT ctxt "C" (rtac @{thm ext}),
     
     (* reflexivity of the basic relations *)
@@ -978,12 +978,17 @@
     DT ctxt "E" (atac),
 
     (* seems not necessay:: DT ctxt "F" (SOLVES' (simp_tac (HOL_ss addsimps @{thms FUN_REL.simps}))),*)
+    
+    (* (R1 ===> R2) (\<dots>) (\<lambda>y\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
+    (* (R1 ===> R2) (\<lambda>x\<dots>) (\<dots>) ----> \<lbrakk>R1 x y\<rbrakk> \<Longrightarrow> R2 (\<dots>x) (\<dots>y) *) 
     DT ctxt "G" (weak_lambda_res_tac ctxt),
 
-    (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed to apply respectfulness theorems *)
-    (* works globally *)
+    (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
+    (* global simplification *)
     DT ctxt "H" (CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ})))])
+*}
 
+ML {*
 fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
   REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms)
 *}