# HG changeset patch
# User hoelzl
# Date 1307621078 -7200
# Node ID acdac535c7fafeae2ab7671948faab5875f6c37b
# Parent  60e181c4eae4d6e43eb0a415fb428a4879d067a7
fixed document generation for HOL

diff -r 60e181c4eae4 -r acdac535c7fa src/HOL/Quickcheck_Narrowing.thy
--- a/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 09 14:04:34 2011 +0200
+++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Jun 09 14:04:38 2011 +0200
@@ -26,7 +26,7 @@
 
 code_reserved Haskell_Quickcheck Typerep
 
-subsubsection {* Type @{text "code_int"} for Haskell_Quickcheck's Int type *}
+subsubsection {* Type @{text "code_int"} for Haskell Quickcheck's Int type *}
 
 typedef (open) code_int = "UNIV \<Colon> int set"
   morphisms int_of of_int by rule
@@ -218,7 +218,7 @@
 datatype narrowing_term = Var "code_int list" narrowing_type | Ctr code_int "narrowing_term list"
 datatype 'a cons = C narrowing_type "(narrowing_term list => 'a) list"
 
-subsubsection {* From narrowing's deep representation of terms to Code_Evaluation's terms *}
+subsubsection {* From narrowing's deep representation of terms to @{theory Code_Evaluation}'s terms *}
 
 class partial_term_of = typerep +
   fixes partial_term_of :: "'a itself => narrowing_term => Code_Evaluation.term"