diff -r d36be1e356c0 -r fff2e1b40dfc thys/Journal/Paper.thy
--- a/thys/Journal/Paper.thy	Tue Jul 18 18:39:20 2017 +0100
+++ b/thys/Journal/Paper.thy	Wed Jul 19 14:55:46 2017 +0100
@@ -52,6 +52,7 @@
   injval ("inj _ _ _" [79,77,79] 76) and 
   mkeps ("mkeps _" [79] 76) and 
   length ("len _" [73] 73) and
+  intlen ("len _" [73] 73) and
  
   Prf ("_ : _" [75,75] 75) and  
   Posix ("'(_, _') \<rightarrow> _" [63,75,75] 75) and
@@ -71,7 +72,7 @@
   lex_list ("_ \<prec>\<^bsub>lex\<^esub> _") and
   PosOrd ("_ \<prec>\<^bsub>_\<^esub> _" [77,77,77] 77) and
   PosOrd_ex ("_ \<prec> _" [77,77] 77) and
-  PosOrd_ex1 ("_ \<^raw:\mbox{$\preccurlyeq$}> _" [77,77] 77) and
+  PosOrd_ex_eq ("_ \<^raw:\mbox{$\preccurlyeq$}> _" [77,77] 77) and
   pflat_len ("\<parallel>_\<parallel>\<^bsub>_\<^esub>") and
   nprec ("_ \<^raw:\mbox{$\not\prec$}> _" [77,77] 77) 
 
@@ -430,9 +431,8 @@
   @{thm[mode=Axiom] Prf.intros(5)[of "c"]}\\[4mm]
   @{thm[mode=Rule] Prf.intros(2)[of "v\<^sub>1" "r\<^sub>1" "r\<^sub>2"]} \qquad 
   @{thm[mode=Rule] Prf.intros(3)[of "v\<^sub>2" "r\<^sub>1" "r\<^sub>2"]}\\[4mm]
-  @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]}\\[4mm]
-  @{thm[mode=Axiom] Prf.intros(6)[of "r"]} \qquad  
-  @{thm[mode=Rule] Prf.intros(7)[of "v" "r" "vs"]}
+  @{thm[mode=Rule] Prf.intros(1)[of "v\<^sub>1" "r\<^sub>1" "v\<^sub>2" "r\<^sub>2"]} \qquad
+  @{thm[mode=Rule] Prf.intros(6)[of "vs"]}
   \end{tabular}
   \end{center}
 
@@ -1098,7 +1098,7 @@
 
  @{thm PosOrd_ex_def[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
 
- @{thm PosOrd_ex1_def[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
+ @{thm PosOrd_ex_eq_def[where ?v1.0="v\<^sub>1" and ?v2.0="v\<^sub>2"]}
 
  Lemma 1