src/HOL/Library/Quickcheck_Narrowing.thy
changeset 41943 12f24ad566ea
parent 41930 1e008cc4883a
child 41961 fdd37cfcd4a3
--- 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