Theory Applicative_Star

(* Author: Andreas Lochbihler, ETH Zurich *)

subsection ‹Ultrafilter›

theory Applicative_Star imports
  Applicative
  "HOL-Nonstandard_Analysis.StarDef"
begin

applicative star (C, K, W)
for
  pure: star_of
  ap: Ifun
proof -
  show "star_of f ⋆ star_of x = star_of (f x)" for f x by(fact Ifun_star_of)
qed(transfer; rule refl)+

end