diff -r 95e7933968f8 -r a88af0e4731f Journal/Paper.thy
--- a/Journal/Paper.thy	Thu Jun 02 13:15:03 2016 +0100
+++ b/Journal/Paper.thy	Tue Jun 07 13:51:39 2016 +0100
@@ -5,6 +5,26 @@
         "~~/src/HOL/Library/LaTeXsugar"
 begin
 
+ML {* Scan.succeed *}
+
+ML {*
+ fun strip_quants ctxt trm =
+   case trm of 
+      Const("HOL.Trueprop", _) $ t => strip_quants ctxt t 
+    | Const("Pure.imp", _) $ _ $ t => strip_quants ctxt t
+    | Const("Pure.all", _) $ Abs(n, T, t) =>
+         strip_quants ctxt (subst_bound (Free (n, T), t)) 
+    | Const("HOL.All", _) $ Abs(n, T, t) =>
+         strip_quants ctxt (subst_bound (Free (n, T), t)) 
+    | Const("HOL.Ex", _) $ Abs(n, T, t) =>
+         strip_quants ctxt (subst_bound (Free (n, T), t)) 
+    | _ => trm
+*}
+
+
+setup {* Term_Style.setup @{binding "no_quants"} (Scan.succeed strip_quants) *}
+
+
 declare [[show_question_marks = false]]
 
 notation (latex output)
@@ -26,6 +46,7 @@
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>") and
   cntP ("c\<^bsub>P\<^esub>") and
   cntV ("c\<^bsub>V\<^esub>")
+
  
 (*>*)
 
@@ -1021,11 +1042,29 @@
   thread is exactly @{term "th'"}.
 
   \begin{lemma}
-  If @{thm (prem 1) th_blockedE_pretty} then
-  @{thm (concl) th_blockedE_pretty}.
+  If @{thm (prem 1) th_blockedE_pretty} then there exists a thread @{text "th'"}
+  such that @{thm (no_quants) th_blockedE_pretty}.
   \end{lemma}
 
   \begin{proof}
+  We know that @{term th} cannot be in @{term readys}, because it has
+  the highest precedence and therefore must be running. This violates our
+  assumption. So by ?? we have that there must be a @{term "th'"} such that
+  @{term "th' \<in> readys (t @ s)"} and @{term "(Th th, Th th') \<in> (RAG (t @ s))\<^sup>+"}.
+  We are going to first show that this @{term "th'"} must be running. For this we 
+  need to show that @{term th'} holds the highest @{term cp}-value.
+  By ?? we know that the @{term "cp"}-value of @{term "th'"} must
+  be the highest all precedences of all thread nodes in its @{term tRAG}-subtree.
+  That is 
+
+  \begin{center}
+  @{term "cp (t @ s) th' = Max (the_preced (t @ s) ` 
+    (the_thread ` subtree (tRAG (t @ s)) (Th th')))"}
+  \end{center}
+
+  But since @{term th} is in this subtree the right-hand side is equal
+  to @{term "preced th (t @ s)"}.
+
   %Let me distinguish between cp (current precedence) and assigned precedence (the precedence the
   %thread ``normally'' has).
   %So we want to show what the cp of th' is in state t @ s.