# HG changeset patch
# User Brian Huffman <brianh@cs.pdx.edu>
# Date 1270710593 25200
# Node ID a862a3befe3745669125ad5f9373bb00b8fc808e
# Parent  ed1dc87d1e3be437e307c2725e5c9bd0d7d9194e
use qualified name as string in concrete atom example

diff -r ed1dc87d1e3b -r a862a3befe37 Pearl/Paper.thy
--- a/Pearl/Paper.thy	Thu Apr 08 00:01:45 2010 -0700
+++ b/Pearl/Paper.thy	Thu Apr 08 00:09:53 2010 -0700
@@ -890,10 +890,10 @@
 
   The following Isabelle/HOL command defines a concrete atom type called
   \emph{name}, which consists of atoms whose sort equals the string @{term
-  "''name''"}.
+  "''Thy.name''"}.
 
   \begin{isabelle}\ \ \ \ \ \ \ \ \ \ %%%
-  \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''name''}"}
+  \isacommand{typedef}\ \ @{typ name} = @{term "{a. sort\<iota> a = ''Thy.name''}"}
   \end{isabelle}
 
   \noindent