Theory Logic_Util

(*
Author:  Christian Sternagel <c.sternagel@gmail.com> (2012-2015)
Author:  René Thiemann <rene.thiemann@uibk.ac.at> (2012-2015)
License: LGPL (see file COPYING.LESSER)
*)
theory Logic_Util
imports
  "$AFP/Matrix/Utility"
begin

lemma ballI2[Pure.intro]:
  assumes "⋀x y. (x, y) ∈ A ⟹ P x y"
  shows "∀(x, y)∈A. P x y"
  using assms by auto

end