--- a/thys/Paper/Paper.thy	Fri Mar 11 10:43:44 2016 +0000
+++ b/thys/Paper/Paper.thy	Fri Mar 11 13:53:53 2016 +0000
@@ -39,7 +39,7 @@
   length ("len _" [78] 73) and
  
   Prf ("_ : _" [75,75] 75) and  
-  PMatch ("'(_, _') \<rightarrow> _" [63,75,75] 75) and
+  Posix ("'(_, _') \<rightarrow> _" [63,75,75] 75) and
  
   lexer ("lexer _ _" [78,78] 77) and 
   F_RIGHT ("F\<^bsub>Right\<^esub> _") and
@@ -586,24 +586,24 @@
 
   \begin{center}
   \begin{tabular}{c}
-  @{thm[mode=Axiom] PMatch.intros(1)}@{text "P"}@{term "ONE"} \qquad
-  @{thm[mode=Axiom] PMatch.intros(2)}@{text "P"}@{term "c"}\bigskip\\
-  @{thm[mode=Rule] PMatch.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}@{text "P+L"}\qquad
-  @{thm[mode=Rule] PMatch.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}@{text "P+R"}\bigskip\\
+  @{thm[mode=Axiom] Posix.intros(1)}@{text "P"}@{term "ONE"} \qquad
+  @{thm[mode=Axiom] Posix.intros(2)}@{text "P"}@{term "c"}\bigskip\\
+  @{thm[mode=Rule] Posix.intros(3)[of "s" "r\<^sub>1" "v" "r\<^sub>2"]}@{text "P+L"}\qquad
+  @{thm[mode=Rule] Posix.intros(4)[of "s" "r\<^sub>2" "v" "r\<^sub>1"]}@{text "P+R"}\bigskip\\
   $\mprset{flushleft}
    \inferrule
-   {@{thm (prem 1) PMatch.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \qquad
-    @{thm (prem 2) PMatch.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \\\\
-    @{thm (prem 3) PMatch.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}
-   {@{thm (concl) PMatch.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}$@{text "PS"}\\
-  @{thm[mode=Axiom] PMatch.intros(7)}@{text "P[]"}\bigskip\\
+   {@{thm (prem 1) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \qquad
+    @{thm (prem 2) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]} \\\\
+    @{thm (prem 3) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}
+   {@{thm (concl) Posix.intros(5)[of "s\<^sub>1" "r\<^sub>1" "v\<^sub>1" "s\<^sub>2" "r\<^sub>2" "v\<^sub>2"]}}$@{text "PS"}\\
+  @{thm[mode=Axiom] Posix.intros(7)}@{text "P[]"}\bigskip\\
   $\mprset{flushleft}
    \inferrule
-   {@{thm (prem 1) PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad
-    @{thm (prem 2) PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad
-    @{thm (prem 3) PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \\\\
-    @{thm (prem 4) PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}
-   {@{thm (concl) PMatch.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}$@{text "P\<star>"}
+   {@{thm (prem 1) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad
+    @{thm (prem 2) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \qquad
+    @{thm (prem 3) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]} \\\\
+    @{thm (prem 4) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}
+   {@{thm (concl) Posix.intros(6)[of "s\<^sub>1" "r" "v" "s\<^sub>2" "vs"]}}$@{text "P\<star>"}
   \end{tabular}
   \end{center}
 
@@ -645,13 +645,13 @@
    v"}.
 
   \begin{theorem}
-  @{thm[mode=IfThen] PMatch_determ(1)[of _ _ "v\<^sub>1" "v\<^sub>2"]}
+  @{thm[mode=IfThen] Posix_determ(1)[of _ _ "v\<^sub>1" "v\<^sub>2"]}
   \end{theorem}
 
   \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"}. This proof requires the
-  auxiliary lemma that @{thm (prem 1) PMatch1(1)} implies @{thm (concl)
-  PMatch1(1)} and @{thm (concl) PMatch1(2)}, which are both easily
+  auxiliary lemma that @{thm (prem 1) Posix1(1)} implies @{thm (concl)
+  Posix1(1)} and @{thm (concl) Posix1(2)}, which are both easily
   established by inductions.\qed \end{proof}
 
   \noindent
@@ -659,7 +659,7 @@
   the POSIX value for the empty string and a nullable regular expression.
 
   \begin{lemma}\label{lemmkeps}
-  @{thm[mode=IfThen] PMatch_mkeps}
+  @{thm[mode=IfThen] Posix_mkeps}
   \end{lemma}
 
   \begin{proof}
@@ -670,8 +670,8 @@
   The central lemma for our POSIX relation is that the @{text inj}-function
   preserves POSIX values.
 
-  \begin{lemma}\label{PMatch2}
-  @{thm[mode=IfThen] PMatch2_roy_version}
+  \begin{lemma}\label{Posix2}
+  @{thm[mode=IfThen] Posix2_roy_version}
   \end{lemma}
 
   \begin{proof}
@@ -730,7 +730,7 @@
   \end{proof}
 
   \noindent
-  With Lem.~\ref{PMatch2} in place, it is completely routine to establish
+  With Lem.~\ref{Posix2} in place, it is completely routine to establish
   that the Sulzmann and Lu lexer satisfies our specification (returning
   an ``error'' iff the string is not in the language of the regular expression,
   and returning a unique POSIX value iff the string \emph{is} in the language):
@@ -743,7 +743,7 @@
   \end{theorem}
 
   \begin{proof}
-  By induction on @{term s} using Lem.~\ref{lemmkeps} and \ref{PMatch2}.\qed  
+  By induction on @{term s} using Lem.~\ref{lemmkeps} and \ref{Posix2}.\qed  
   \end{proof}
 
   \noindent This concludes our correctness proof. Note that we have not