diff -r 704fd8749dad -r ca4ddf26a7c7 Journal/Paper.thy
--- a/Journal/Paper.thy	Thu Sep 21 14:33:13 2017 +0100
+++ b/Journal/Paper.thy	Fri Sep 22 03:08:30 2017 +0100
@@ -28,34 +28,40 @@
 declare [[show_question_marks = false]]
 
 notation (latex output)
-  Cons ("_::_" [78,77] 73) and
-  If  ("(\<^raw:\textrm{>if\<^raw:}> (_)/ \<^raw:\textrm{>then\<^raw:}> (_)/ \<^raw:\textrm{>else\<^raw:}> (_))" 10) and
+  Cons ("_::_" [78,77] 73)
+
+notation (latex output)
   vt ("valid'_state") and
   Prc ("'(_, _')") and
   holding_raw ("holds") and
   holding ("holds") and
-  waiting_raw ("waits") and
+  waiting_raw ("waits")
+
+notation (latex output)
   waiting ("waits") and
   tG_raw ("TDG") and
   tG ("TDG") and
-  RAG_raw ("RAG") and
+  RAG_raw ("RAG") and 
   RAG ("RAG") and
-  Th ("T") and
+  Th ("T") 
+
+notation (latex output)
   Cs ("C") and
   readys ("ready") and
   preced ("prec") and
   preceds ("precs") and
   cpreced ("cprec") and
   cpreceds ("cprecs") and
-  (*wq_fun ("wq") and*)
   cp ("cprec") and
-  (*cprec_fun ("cp_fun") and*)
-  holdents ("resources") and
-  DUMMY  ("\<^raw:\mbox{$\_\!\_$}>") and
+  holdents ("resources") and  
   cntP ("c\<^bsub>P\<^esub>") and
   cntV ("c\<^bsub>V\<^esub>")
 
- 
+notation (latex output)
+  DUMMY  ("\<^latex>\<open>\\mbox{$\\_\\!\\_$}\<close>")
+
+notation (latex output)
+  If  ("(\<^latex>\<open>\\textrm{\<close>if\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>then\<^latex>\<open>}\<close> (_)/ \<^latex>\<open>\\textrm{\<close>else\<^latex>\<open>}\<close> (_))" 10)
 (*>*)
 
 section {* Introduction *}