# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1259290940 -3600
# Node ID f79dd55008386d4d1000673215ac85d3ce7d5094
# Parent  54d3c72ddd0567a1a94952b044ee6a79fb29bc8e
tuned

diff -r 54d3c72ddd05 -r f79dd5500838 QuotMain.thy
--- a/QuotMain.thy	Fri Nov 27 03:56:18 2009 +0100
+++ b/QuotMain.thy	Fri Nov 27 04:02:20 2009 +0100
@@ -1070,9 +1070,6 @@
 
 section {* General outline of the lifting procedure *}
 
-
-(* **************************************** *)
-(*                                          *)
 (* - A is the original raw theorem          *)
 (* - B is the regularized theorem           *)
 (* - C is the rep/abs injected version of B *) 
@@ -1082,7 +1079,7 @@
 (* - c is the rep/abs injection step        *)
 (* - d is the cleaning part                 *)
 
-lemma procedure:
+lemma lifting_procedure:
   assumes a: "A"
   and     b: "A \<Longrightarrow> B"
   and     c: "B = C"
@@ -1119,7 +1116,7 @@
   Drule.instantiate' []
     [SOME (cterm_of thy rtrm'),
      SOME (cterm_of thy reg_goal),
-     SOME (cterm_of thy inj_goal)] @{thm procedure}
+     SOME (cterm_of thy inj_goal)] @{thm lifting_procedure}
 end
 *}
 
@@ -1138,6 +1135,7 @@
 *}
 
 ML {*
+(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
 fun lift_tac lthy rthm rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs =
   ObjectLogic.full_atomize_tac
   THEN' gen_frees_tac lthy
@@ -1147,11 +1145,12 @@
       val rule = procedure_inst context (prop_of rthm') (term_of concl)
       val aps = find_aps (prop_of rthm') (term_of concl)
     in
-      EVERY1 [rtac rule, 
-              RANGE [rtac rthm',
-                     regularize_tac lthy [rel_eqv] rel_refl,
-                     REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
-                     clean_tac lthy quot defs reps_same absrep aps]] 
+      EVERY1 
+       [rtac rule, 
+        RANGE [rtac rthm',
+               regularize_tac lthy [rel_eqv] rel_refl,
+               REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
+               clean_tac lthy quot defs reps_same absrep aps]] 
     end) lthy
 *}