File ‹zippy_ctxt_state_mixin_base.ML›

(*  Title:      Zippy/zippy_ctxt_state_mixin_base.ML
    Author:     Kevin Kappelmann
*)
signature ZIPPY_CTXT_STATE_MIXIN_BASE =
sig
  include \<^eval>‹sfx_ParaT_nargs "MORPH_BASE"›
  structure MS : \<^eval>‹sfx_ParaT_nargs "MONAD_STATE_BASE"›
  where type s = Proof.context
  sharing type MS.t = M.t
end

functor Zippy_Ctxt_State_Mixin_Base(
    MS : \<^eval>‹sfx_ParaT_nargs "MONAD_STATE_BASE"›
    where type s = Proof.context
  ) : ZIPPY_CTXT_STATE_MIXIN_BASE
  =
struct
structure MS = MS
structure MB = \<^eval>‹sfx_ParaT_nargs "Morph_Base"›(MS)
open MB
end