--- a/src/HOL/Library/Quickcheck_Narrowing.thy Sun Mar 13 15:13:53 2011 +0100
+++ b/src/HOL/Library/Quickcheck_Narrowing.thy Sun Mar 13 15:16:37 2011 +0100
@@ -19,7 +19,7 @@
code_reserved Haskell Typerep
-subsubsection {* Type code_int for Haskell's Int type *}
+subsubsection {* Type @{text code_int} for Haskell's Int type *}
typedef (open) code_int = "UNIV \<Colon> int set"
morphisms int_of of_int by rule
@@ -325,9 +325,9 @@
end
-subsubsection {* class is_testable *}
+subsubsection {* class @{text is_testable} *}
-text {* The class is_testable ensures that all necessary type instances are generated. *}
+text {* The class @{text is_testable} ensures that all necessary type instances are generated. *}
class is_testable