diff -r 42671298f037 -r 313a24b66a8d doc-src/TutorialI/Rules/document/find2.tex
--- a/doc-src/TutorialI/Rules/document/find2.tex	Sun Nov 07 23:32:26 2010 +0100
+++ b/doc-src/TutorialI/Rules/document/find2.tex	Mon Nov 08 00:00:47 2010 +0100
@@ -31,10 +31,10 @@
 \texttt{intro}, \texttt{elim} and \texttt{dest}.
 
 For example, given the goal \begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ A\ {\isasymand}\ B%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B%
 \end{isabelle}
 you can click on \pgmenu{Find} and type in the search expression
-\texttt{intro}. You will be shown a few rules ending in \isa{{\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q},
+\texttt{intro}. You will be shown a few rules ending in \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}Q},
 among them \isa{conjI}\@. You may even discover that
 the very theorem you are trying to prove is already in the
 database.  Given the goal%
@@ -57,17 +57,17 @@
 \begin{isamarkuptxt}%
 \vspace{-\bigskipamount}
 \begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ A\ {\isasymlongrightarrow}\ A%
+\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ A%
 \end{isabelle}
 the search for \texttt{intro} finds not just \isa{impI}
-but also \isa{imp{\isacharunderscore}refl}: \isa{{\isacharquery}P\ {\isasymlongrightarrow}\ {\isacharquery}P}.
+but also \isa{imp{\isaliteral{5F}{\isacharunderscore}}refl}: \isa{{\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P}.
 
 As before, search criteria can be combined freely: for example,
 \begin{ttbox}
 "_ \at\ _"  intro
 \end{ttbox}
 searches for all introduction rules that match the current goal and
-mention the \isa{{\isacharat}} function.
+mention the \isa{{\isaliteral{40}{\isacharat}}} function.
 
 Searching for elimination and destruction rules via \texttt{elim} and
 \texttt{dest} is analogous to \texttt{intro} but takes the assumptions