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