--- a/thys/Paper/Paper.thy	Mon Mar 07 21:54:50 2016 +0000
+++ b/thys/Paper/Paper.thy	Mon Mar 07 22:20:15 2016 +0000
@@ -541,7 +541,7 @@
   \begin{proof}
   Both properties are by routine inductions: the first one, for example,
   by an induction over the definition of @{term derivatives}; the second by
-  induction on @{term r}. There are no interesting cases.
+  induction on @{term r}. There are no interesting cases.\qed
   \end{proof}
 
   Having defined the @{const mkeps} and @{text inj} function we can extend
@@ -641,14 +641,16 @@
 
   \begin{proof}
   By induction on the definition of @{term "s \<in> r \<rightarrow> v\<^sub>1"} and a case
-  analysis of @{term "s \<in> r \<rightarrow> v\<^sub>2"}.
+  analysis of @{term "s \<in> r \<rightarrow> v\<^sub>2"}.\qed
   \end{proof}
 
   \begin{lemma}
   @{thm[mode=IfThen] PMatch_mkeps}
   \end{lemma}
 
-  
+  \begin{proof}
+  By routine induction on @{term r}.\qed 
+  \end{proof}
 
   \begin{lemma}
   @{thm[mode=IfThen] PMatch2_roy_version}