| changeset 46062 | 9bc924006136 |
| parent 45970 | b6d0cff57d96 |
| child 46072 | 291c14a01b6d |
--- a/src/HOL/Metis_Examples/Proxies.thy Sat Dec 31 00:19:32 2011 +0100 +++ b/src/HOL/Metis_Examples/Proxies.thy Sat Dec 31 10:15:53 2011 +0100 @@ -40,7 +40,7 @@ definition "A = {xs\<Colon>'a list. True}" lemma "xs \<in> A" -sledgehammer [expect = some] +sledgehammer(* FIXME [expect = some] *) by (metis_exhaust A_def mem_Collect_eq) definition "B (y::int) \<equiv> y \<le> 0"