# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1260417754 -3600
# Node ID 44fe82707e0e9ce77940c55dcb36f7944463da89
# Parent  fa0f6fdac5de4fd68ff8cb8ccb6f31305d3fe83e
tuned

diff -r fa0f6fdac5de -r 44fe82707e0e Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Thu Dec 10 04:53:48 2009 +0100
+++ b/Quot/QuotMain.thy	Thu Dec 10 05:02:34 2009 +0100
@@ -665,9 +665,6 @@
   and   QT_ext: "(\<And>x. QUOT_TRUE (a x) \<Longrightarrow> f x = g x) \<Longrightarrow> (QUOT_TRUE a \<Longrightarrow> f = g)"
 by (simp_all add: QUOT_TRUE_def ext)
 
-lemma QUOT_TRUE_i: "(QUOT_TRUE (a :: bool) \<Longrightarrow> P) \<Longrightarrow> P"
-by (simp add: QUOT_TRUE_def)
-
 lemma QUOT_TRUE_imp: "QUOT_TRUE a \<equiv> QUOT_TRUE b"
 by (simp add: QUOT_TRUE_def)
 
@@ -1014,7 +1011,7 @@
   end
 *}
 
-section {* Tactic for genralisation of free variables in a goal *}
+section {* Tactic for Genralisation of Free Variables in a Goal *}
 
 ML {*
 fun inst_spec ctrm =
@@ -1046,14 +1043,16 @@
 
 section {* General Shape of the Lifting Procedure *}
 
-(* - A is the original raw theorem          *)
-(* - B is the regularized theorem           *)
-(* - C is the rep/abs injected version of B *) 
-(* - D is the lifted theorem                *)
-(*                                          *)
-(* - b is the regularization step           *)
-(* - c is the rep/abs injection step        *)
-(* - d is the cleaning part                 *)
+(* - A is the original raw theorem                  *)
+(* - B is the regularized theorem                   *)
+(* - C is the rep/abs injected version of B         *) 
+(* - D is the lifted theorem                        *)
+(*                                                  *)
+(* - b is the regularization step                   *)
+(* - c is the rep/abs injection step                *)
+(* - d is the cleaning part                         *)
+(*                                                  *)
+(* the QUOT_TRUE premise records the lifted theorem *)
 
 lemma lifting_procedure:
   assumes a: "A"
@@ -1111,7 +1110,8 @@
     end)
 *}
 
-(* automatic proofs *)
+section {* Automatic Proofs *}
+
 ML {*
 fun SOLVES' tac = tac THEN_ALL_NEW (K no_tac)
 
@@ -1132,7 +1132,8 @@
       (clean_tac ctxt,          "Cleaning proof failed.")]
 *}
 
-section {* methods / interface *}
+section {* Methods / Interface *}
+
 ML {*
 fun mk_method1 tac thm ctxt =
   SIMPLE_METHOD (HEADGOAL (tac ctxt thm))