# HG changeset patch
# User haftmann
# Date 1174979977 -7200
# Node ID 84690fcd3db91a2d6148aae7bd2fc658b702eaa5
# Parent  be2269950fe56e7a0eb4264ea7fb9a1b27fd06e4
fixed document preparation

diff -r be2269950fe5 -r 84690fcd3db9 src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Mon Mar 26 16:35:33 2007 +0200
+++ b/src/HOL/Library/Eval.thy	Tue Mar 27 09:19:37 2007 +0200
@@ -9,7 +9,7 @@
 imports Pure_term
 begin
 
-subsection {* The typ_of class *}
+subsection {* @{text typ_of} class *}
 
 class typ_of = type +
   fixes typ_of :: "'a itself \<Rightarrow> typ"
@@ -48,7 +48,7 @@
 *}
 
 
-subsection {* term_of class *}
+subsection {* @{text term_of} class *}
 
 class term_of = typ_of +
   constrains typ_of :: "'a itself \<Rightarrow> typ"
@@ -109,7 +109,7 @@
 in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
 *}
 
-text {* Disable for characters and ml_strings *}
+text {* Disable for @{typ char}acters and @{typ ml_string}s *}
 
 code_const "typ_of \<Colon> char itself \<Rightarrow> typ" and "term_of \<Colon> char \<Rightarrow> term"
   (SML "!((_); raise Fail \"typ'_of'_char\")"