# HG changeset patch
# User urbanc
# Date 1298259339 0
# Node ID 06bafc71042305585ff9ccd63814da76be5d158e
# Parent  13b0f3dac9a2287fff67b92cce790318634d9a91
one further polishing

diff -r 13b0f3dac9a2 -r 06bafc710423 Paper/Paper.thy
--- a/Paper/Paper.thy	Mon Feb 21 03:33:27 2011 +0000
+++ b/Paper/Paper.thy	Mon Feb 21 03:35:39 2011 +0000
@@ -1161,7 +1161,7 @@
   
   \noindent
   The case for @{const STAR} is similar to @{const SEQ}, but poses a few extra challenges. When
-  we analyse the case that @{text "x @ z"} is an element in @{text "A\<star>"} and @{text x} is not the 
+  we analyse the case that @{text "x @ z"} is an element in @{term "A\<star>"} and @{text x} is not the 
   empty string, we 
   have the following picture:
   %