author | blanchet |
Mon, 07 May 2012 14:50:49 +0200 (2012-05-07) | |
changeset 47892 | e389889da7df |
parent 47891 | e3627a83b114 |
child 47893 | 4cf901b1089a |
--- a/src/HOL/Metis_Examples/Proxies.thy Mon May 07 12:20:55 2012 +0200 +++ b/src/HOL/Metis_Examples/Proxies.thy Mon May 07 14:50:49 2012 +0200 @@ -34,7 +34,7 @@ "add_swap = (\<lambda>x y. y + x)" lemma "add_swap m n = n + m" -sledgehammer [expect = some] +sledgehammer [expect = some] (add_swap_def) by (metis_exhaust add_swap_def) definition "A = {xs\<Colon>'a list. True}"