diff -r 97090fc7aa9f -r 560712a29a36 Journal/Paper.thy
--- a/Journal/Paper.thy	Sun Jul 31 10:27:41 2011 +0000
+++ b/Journal/Paper.thy	Tue Aug 02 15:27:37 2011 +0000
@@ -1,6 +1,6 @@
 (*<*)
 theory Paper
-imports "../Closures" 
+imports "../Closures" "../Attic/Prefix_subtract" 
 begin
 
 declare [[show_question_marks = false]]
@@ -1290,15 +1290,7 @@
   %
   \noindent
   and \emph{string subtraction}:
-  %
-  \begin{center}
-  \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
-  @{text "[] - y"}  & @{text "\<equiv>"} & @{text "[]"}\\
-  @{text "x - []"}  & @{text "\<equiv>"} & @{text "x"}\\
-  @{text "cx - dy"} & @{text "\<equiv>"} & @{text "if c = d then x - y else cx"}
-  \end{tabular}
-  \end{center}
-  %
+
   \noindent
   where @{text c} and @{text d} are characters, and @{text x} and @{text y} are strings.