| changeset 57260 | 8747af0d1012 |
| parent 56677 | 660ffb526069 |
| child 57398 | 882091eb1e9a |
--- a/src/HOL/Transfer.thy Mon Jun 16 17:52:33 2014 +0200 +++ b/src/HOL/Transfer.thy Mon Jun 16 19:18:10 2014 +0200 @@ -246,7 +246,7 @@ using assms by (auto simp add: eq_onp_def) lemma Ball_Collect: "Ball A P = (A \<subseteq> (Collect P))" -by (metis mem_Collect_eq subset_eq) +by auto ML_file "Tools/Transfer/transfer.ML" setup Transfer.setup