src/HOL/Quickcheck_Narrowing.thy
changeset 61799 4cf66f21b764
parent 60758 d8d85a8172b5
child 65480 5407bc278c9a
     1.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -155,9 +155,9 @@
     1.4  where
     1.5    "all f = (case narrowing (100 :: integer) of Narrowing_cons ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))"
     1.6  
     1.7 -subsubsection \<open>class @{text is_testable}\<close>
     1.8 +subsubsection \<open>class \<open>is_testable\<close>\<close>
     1.9  
    1.10 -text \<open>The class @{text is_testable} ensures that all necessary type instances are generated.\<close>
    1.11 +text \<open>The class \<open>is_testable\<close> ensures that all necessary type instances are generated.\<close>
    1.12  
    1.13  class is_testable
    1.14  
    1.15 @@ -319,7 +319,7 @@
    1.16             (Generated'_Code.Const \"Groups.uminus'_class.uminus\" (mkFunT t t))
    1.17             (mkNumber (- i)); } in mkNumber)"
    1.18  
    1.19 -subsection \<open>The @{text find_unused_assms} command\<close>
    1.20 +subsection \<open>The \<open>find_unused_assms\<close> command\<close>
    1.21  
    1.22  ML_file "Tools/Quickcheck/find_unused_assms.ML"
    1.23