# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260668867 -3600
# Node ID 198ff5781844c0359ac55e3204400c8a180eca04
# Parent  8437359e811c382fef2e94c11c248b9a635aa0fa
a few code annotations

diff -r 8437359e811c -r 198ff5781844 Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Sun Dec 13 02:35:34 2009 +0100
+++ b/Quot/QuotMain.thy	Sun Dec 13 02:47:47 2009 +0100
@@ -397,6 +397,7 @@
     (Const (@{const_name "Ball"}, _) $ (Const (@{const_name "Respects"}, _) $ 
       (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>
         calculate_instance ctxt @{thm ball_reg_eqv_range} redex R1 R2
+
   | (Const (@{const_name "Bex"}, _) $ (Const (@{const_name "Respects"}, _) $ 
       (Const (@{const_name "fun_rel"}, _) $ R1 $ R2)) $ _) =>  
         calculate_instance ctxt @{thm bex_reg_eqv_range} redex R1 R2
@@ -552,8 +553,6 @@
 
 section {* Injection Tactic *}
 
-
-
 definition
   "QUOT_TRUE x \<equiv> True"
 
@@ -715,11 +714,11 @@
            val (ty_a, ty_b) = dest_fun_type (fastype_of abs);
            val ty_inst = map (SOME o (ctyp_of thy)) [ty_a, ty_b];
            val t_inst = map (SOME o (cterm_of thy)) [rel, abs, rep];
-           val thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
+           val inst_thm = Drule.instantiate' ty_inst t_inst @{thm rep_abs_rsp}
          in
-           (rtac thm THEN' quotient_tac ctxt) i
+           (rtac inst_thm THEN' quotient_tac ctxt) i
          end
-         handle _ => no_tac) (* what is the catch for ? Should go away, no? *)
+         handle _ => no_tac) (* FIXME / TODO what is the catch for ? Should go away, no? *)
     | _ => no_tac)
 *}
 
@@ -871,6 +870,8 @@
 *}
 
 ML {*
+(* FIXME / TODO this needs to be clarified *)
+
 fun lambda_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
    (Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _) =>
@@ -1002,7 +1003,11 @@
 
 ML {*
 val lifting_procedure = 
-   @{lemma  "\<lbrakk>A; A \<longrightarrow> B; QUOT_TRUE D \<Longrightarrow> B = C; C = D\<rbrakk> \<Longrightarrow> D" by (simp add: QUOT_TRUE_def)}
+   @{lemma  "\<lbrakk>A; 
+              A \<longrightarrow> B; 
+              QUOT_TRUE D \<Longrightarrow> B = C; 
+              C = D\<rbrakk> \<Longrightarrow> D" 
+             by (simp add: QUOT_TRUE_def)}
 *}
 
 ML {*