(*
Auction Theory Toolbox (http://formare.github.io/auctions/)
Authors:
* Christoph Lange
Dually licenced under
* Creative Commons Attribution (CC-BY) 3.0
* ISC License (1-clause BSD License)
See LICENSE file for details
(Rationale for this dual licence: http://arxiv.org/abs/1107.3212)
*)
header {* Additional material that we would have expected in HOL.thy *}
theory HOLUtils
imports
HOL
begin
text {* An inference rule that combines @{thm allI} and @{thm impI} to a single step *}
lemma allImpI: "(\ x . p x \ q x) \ \ x . p x \ q x" by simp
end