fixed document preparation
authorhaftmann
Tue Mar 27 09:19:37 2007 +0200 (2007-03-27)
changeset 2252784690fcd3db9
parent 22526 be2269950fe5
child 22528 8501c4a62a3c
fixed document preparation
src/HOL/Library/Eval.thy
     1.1 --- a/src/HOL/Library/Eval.thy	Mon Mar 26 16:35:33 2007 +0200
     1.2 +++ b/src/HOL/Library/Eval.thy	Tue Mar 27 09:19:37 2007 +0200
     1.3 @@ -9,7 +9,7 @@
     1.4  imports Pure_term
     1.5  begin
     1.6  
     1.7 -subsection {* The typ_of class *}
     1.8 +subsection {* @{text typ_of} class *}
     1.9  
    1.10  class typ_of = type +
    1.11    fixes typ_of :: "'a itself \<Rightarrow> typ"
    1.12 @@ -48,7 +48,7 @@
    1.13  *}
    1.14  
    1.15  
    1.16 -subsection {* term_of class *}
    1.17 +subsection {* @{text term_of} class *}
    1.18  
    1.19  class term_of = typ_of +
    1.20    constrains typ_of :: "'a itself \<Rightarrow> typ"
    1.21 @@ -109,7 +109,7 @@
    1.22  in DatatypeCodegen.add_codetypes_hook_bootstrap hook end
    1.23  *}
    1.24  
    1.25 -text {* Disable for characters and ml_strings *}
    1.26 +text {* Disable for @{typ char}acters and @{typ ml_string}s *}
    1.27  
    1.28  code_const "typ_of \<Colon> char itself \<Rightarrow> typ" and "term_of \<Colon> char \<Rightarrow> term"
    1.29    (SML "!((_); raise Fail \"typ'_of'_char\")"