# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259286251 -3600
# Node ID d387743f022bd1de1449306e9288f6cb00d2104f
# Parent  f32237ef18a6f59f498050671b66fe63a95869d8
tuned comments and moved slightly some code

diff -r f32237ef18a6 -r d387743f022b QuotMain.thy
--- a/QuotMain.thy	Fri Nov 27 02:35:50 2009 +0100
+++ b/QuotMain.thy	Fri Nov 27 02:44:11 2009 +0100
@@ -230,9 +230,26 @@
 end
 *}
 
-section {* Does the same as 'subst' in a given theorem *}
+section {* Debugging infrastructure for testing tactics *}
 
 ML {*
+fun my_print_tac ctxt s thm =
+let
+  val prems_str = prems_of thm
+                  |> map (Syntax.string_of_term ctxt)
+                  |> cat_lines
+  val _ = tracing (s ^ "\n" ^ prems_str)
+in
+  Seq.single thm
+end
+
+fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))]
+*}
+
+section {*  Infrastructure about definitions *}
+
+(* Does the same as 'subst' in a given theorem *)
+ML {*
 fun eqsubst_thm ctxt thms thm =
   let
     val goalstate = Goal.init (Thm.cprop_of thm)
@@ -248,8 +265,6 @@
   end
 *}
 
-section {*  Infrastructure about definitions *}
-
 (* expects atomized definitions *)
 ML {*
 fun add_lower_defs_aux lthy thm =
@@ -274,7 +289,7 @@
   end
 *}
 
-section {* Infrastructure for collecting theorems for calling lifting *}
+section {* Infrastructure for collecting theorems for starting the lifting *}
 
 ML {*
 fun lookup_quot_data lthy qty =
@@ -361,8 +376,10 @@
               (* FIXME: check in this case that the rty and qty *)
               (* FIXME: correspond to each other *)
               val (s, _) = dest_Const (#rel qinfo)
-              (* FIXME: the relation should only be the string       *)
-              (* FIXME: and the type needs to be calculated as below *) 
+              (* FIXME: the relation should only be the string        *)
+              (* FIXME: and the type needs to be calculated as below; *)
+              (* FIXME: maybe one should actually have a term         *)
+              (* FIXME: and one needs to force it to have this type   *)
             in
               Const (s, rty --> rty --> @{typ bool})
             end
@@ -454,6 +471,8 @@
 *}
 
 (*
+FIXME / TODO: needs to be adapted
+
 To prove that the raw theorem implies the regularised one, 
 we try in order:
 
@@ -479,20 +498,6 @@
 
 (* version of regularize_tac including debugging information *)
 ML {*
-fun my_print_tac ctxt s thm =
-let
-  val prems_str = prems_of thm
-                  |> map (Syntax.string_of_term ctxt)
-                  |> cat_lines
-  val _ = tracing (s ^ "\n" ^ prems_str)
-in
-  Seq.single thm
-end
-
-fun DT ctxt s tac = EVERY' [tac, K (my_print_tac ctxt ("after " ^ s))]
-*}
-
-ML {*
 fun regularize_tac ctxt rel_eqv rel_refl =
   (ObjectLogic.full_atomize_tac) THEN'
   REPEAT_ALL_NEW (FIRST'