equal
deleted
inserted
replaced
153 |
153 |
154 definition "all" :: "('a :: {narrowing, partial_term_of} => property) => property" |
154 definition "all" :: "('a :: {narrowing, partial_term_of} => property) => property" |
155 where |
155 where |
156 "all f = (case narrowing (100 :: integer) of Narrowing_cons ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))" |
156 "all f = (case narrowing (100 :: integer) of Narrowing_cons ty cs => Universal ty (\<lambda>t. f (conv cs t)) (partial_term_of (TYPE('a))))" |
157 |
157 |
158 subsubsection \<open>class @{text is_testable}\<close> |
158 subsubsection \<open>class \<open>is_testable\<close>\<close> |
159 |
159 |
160 text \<open>The class @{text is_testable} ensures that all necessary type instances are generated.\<close> |
160 text \<open>The class \<open>is_testable\<close> ensures that all necessary type instances are generated.\<close> |
161 |
161 |
162 class is_testable |
162 class is_testable |
163 |
163 |
164 instance bool :: is_testable .. |
164 instance bool :: is_testable .. |
165 |
165 |
317 else |
317 else |
318 Generated'_Code.App |
318 Generated'_Code.App |
319 (Generated'_Code.Const \"Groups.uminus'_class.uminus\" (mkFunT t t)) |
319 (Generated'_Code.Const \"Groups.uminus'_class.uminus\" (mkFunT t t)) |
320 (mkNumber (- i)); } in mkNumber)" |
320 (mkNumber (- i)); } in mkNumber)" |
321 |
321 |
322 subsection \<open>The @{text find_unused_assms} command\<close> |
322 subsection \<open>The \<open>find_unused_assms\<close> command\<close> |
323 |
323 |
324 ML_file "Tools/Quickcheck/find_unused_assms.ML" |
324 ML_file "Tools/Quickcheck/find_unused_assms.ML" |
325 |
325 |
326 subsection \<open>Closing up\<close> |
326 subsection \<open>Closing up\<close> |
327 |
327 |