# HG changeset patch
# User urbanc
# Date 1298259207 0
# Node ID 13b0f3dac9a2287fff67b92cce790318634d9a91
# Parent  604518f0127f4485f8eaf87731b5d263c4fb6e45
final final polishing

diff -r 604518f0127f -r 13b0f3dac9a2 Paper/Paper.thy
--- a/Paper/Paper.thy	Mon Feb 21 03:30:38 2011 +0000
+++ b/Paper/Paper.thy	Mon Feb 21 03:33:27 2011 +0000
@@ -1191,15 +1191,15 @@
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(xa.south east)+(0em,0ex)$) -- ($(xa.south west)+(0em,0ex)$)
-               node[midway, below=0.5em]{@{text "x'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"}};
+               node[midway, below=0.5em]{@{term "x'\<^isub>m\<^isub>a\<^isub>x \<in> A\<star>"}};
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(zb.south east)+(0em,0ex)$) -- ($(zb.south west)+(0em,0ex)$)
-               node[midway, below=0.5em]{@{text "z\<^isub>b \<in> A\<star>"}};
+               node[midway, below=0.5em]{@{term "z\<^isub>b \<in> A\<star>"}};
 
     \draw[decoration={brace,transform={yscale=3}},decorate]
            ($(zb.south east)+(0em,-4ex)$) -- ($(xxa.south west)+(0em,-4ex)$)
-               node[midway, below=0.5em]{@{text "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}};
+               node[midway, below=0.5em]{@{term "(x - x'\<^isub>m\<^isub>a\<^isub>x) @ z \<in> A\<star>"}};
   \end{tikzpicture}}
   \end{center}
   %