# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1493993010 -3600
# Node ID 5697bb5b6b2bf8d63bc23374f3e1e0c4fc0ff0b3
# Parent  1a67f60a06af65f07bc37babc74c5b3593fddcc8
updated

diff -r 1a67f60a06af -r 5697bb5b6b2b Journal/Paper.thy
--- a/Journal/Paper.thy	Fri May 05 14:53:56 2017 +0100
+++ b/Journal/Paper.thy	Fri May 05 15:03:30 2017 +0100
@@ -1188,86 +1188,86 @@
 
   %\endnote{
   
-In what follows we will describe properties of PIP that allow us to
-  prove Theorem~\ref{mainthm} and, when instructive, briefly describe
-  our argument. Recall we want to prove that in state @ {term "s' @ s"} 
-either @{term th} is either running or blocked by a thread @
-  {term "th'"} (@{term "th \<noteq> th'"}) which was alive in state
-  @{term s}. We can show that
+%In what follows we will describe properties of PIP that allow us to
+%  prove Theorem~\ref{mainthm} and, when instructive, briefly describe
+%  our argument. Recall we want to prove that in state @ {term "s' @ s"} 
+%either @{term th} is either running or blocked by a thread @
+%  {term "th'"} (@{term "th \<noteq> th'"}) which was alive in state
+%  @{term s}. We can show that
 
 
-  \begin{lemma}
-  If @{thm (prem 2) eq_pv_blocked}
-  then @{thm (concl) eq_pv_blocked}
-  \end{lemma}
+%  \begin{lemma}
+%  If @{thm (prem 2) eq_pv_blocked}
+%  then @{thm (concl) eq_pv_blocked}
+%  \end{lemma}
 
-  \begin{lemma}
-  If @{thm (prem 2) eq_pv_persist}
-  then @{thm (concl) eq_pv_persist}
-  \end{lemma}
+%  \begin{lemma}
+%  If @{thm (prem 2) eq_pv_persist}
+%  then @{thm (concl) eq_pv_persist}
+%  \end{lemma}
   %%%}
 
 %  \endnote{{\bf OUTLINE}
 
-  Since @{term "th"} is the most urgent thread, if it is somehow
-  blocked, people want to know why and wether this blocking is
-  reasonable.
+%  Since @{term "th"} is the most urgent thread, if it is somehow
+%  blocked, people want to know why and wether this blocking is
+%  reasonable.
 
-  @{thm [source] th_blockedE} @{thm th_blockedE}
+%  @{thm [source] th_blockedE} @{thm th_blockedE}
 
-  if @{term "th"} is blocked, then there is a path leading from 
-  @{term "th"} to @{term "th'"}, which means:
-  there is a chain of demand leading from @{term th} to @{term th'}.
+%  if @{term "th"} is blocked, then there is a path leading from 
+%  @{term "th"} to @{term "th'"}, which means:
+%  there is a chain of demand leading from @{term th} to @{term th'}.
 
-   in other words
-   th -> cs1 -> th1 -> cs2 -> th2 -> ... -> csn -> thn -> cs -> th'. 
+%   in other words
+%   th -> cs1 -> th1 -> cs2 -> th2 -> ... -> csn -> thn -> cs -> th'. 
    
-   We says that th is blocked by @{text "th'"}.
+%   We says that th is blocked by @{text "th'"}.
 
-  THEN
+%  THEN
 
-  @{thm [source] vat_t.th_chain_to_ready} @{thm vat_t.th_chain_to_ready}
+%  @{thm [source] vat_t.th_chain_to_ready} @{thm vat_t.th_chain_to_ready}
 
-  It is basic propery with non-trival proof. 
+%  It is basic propery with non-trival proof. 
 
-  THEN
+%  THEN
 
-  @{thm [source] max_preced} @{thm max_preced}
+%  @{thm [source] max_preced} @{thm max_preced}
 
-  which says @{term "th"} holds the max precedence.
+%  which says @{term "th"} holds the max precedence.
 
-  THEN
+%  THEN
  
-  @{thm [source] th_cp_max th_cp_preced th_kept}
-  @{thm th_cp_max th_cp_preced th_kept}
+%  @ {thm [source] th_cp_max th_cp_preced th_kept}
+%  @ {thm th_cp_max th_cp_preced th_kept}
 
-  THEN
+%  THEN
 
- ??? %%@ {thm [source] running_inversion_4} @  {thm running_inversion_4}
+% ??? %%@ {thm [source] running_inversion_4} @  {thm running_inversion_4}
 
- which explains what the @{term "th'"} looks like. Now, we have found the 
- @{term "th'"} which blocks @{term th}, we need to know more about it.
- To see what kind of thread can block @{term th}.
+% which explains what the @{term "th'"} looks like. Now, we have found the 
+% @{term "th'"} which blocks @{term th}, we need to know more about it.
+% To see what kind of thread can block @{term th}.
 
-  From these two lemmas we can see the correctness of PIP, which is
-  that: the blockage of th is reasonable and under control.
+%  From these two lemmas we can see the correctness of PIP, which is
+%  that: the blockage of th is reasonable and under control.
 
-  Lemmas we want to describe:
+%  Lemmas we want to describe:
 
-  \begin{lemma}
-  @{thm running_cntP_cntV_inv}
-  \end{lemma}
+%  \begin{lemma}
+%  @{thm running_cntP_cntV_inv}
+%  \end{lemma}
 
-  \noindent
-  Remember we do not have the well-nestedness restriction in our
-  proof, which means the difference between the counters @{const cntV}
-  and @{const cntP} can be larger than @{term 1}.
+%  \noindent
+%  Remember we do not have the well-nestedness restriction in our
+%  proof, which means the difference between the counters @{const cntV}
+%  and @{const cntP} can be larger than @{term 1}.
 
-  \begin{lemma}\label{runninginversion}
-  @{thm running_inversion}
-  \end{lemma}
+%  \begin{lemma}\label{runninginversion}
+%  @ {thm running_inversion}
+%  \end{lemma}
   
-  explain tRAG
+%  explain tRAG
 %}
 
   
diff -r 1a67f60a06af -r 5697bb5b6b2b journal.pdf
Binary file journal.pdf has changed