Q: What exactly is a power admissible model?
Background: Admissible models, introduced by Jon Barwise, form the building blocks of inner model theory. They are transitive models $\mathcal M = (M; \in)$ satisfying a suitable fragment of set theory, namely Kripke-Platek set theory. Sifting through a couple of papers by John Steel, the term power admissible model sprung up a few times and since no definition or reference was given, I more or less assumed that they were just admissible models with enough closure properties such that the given argument would work.
Today I decided to take a closer look at them and after some online research I found a definition of power admissible sets in Cook, Rathjen. Classifying the Provably Total set Functions of $\operatorname{KP}$ and $\operatorname{KP}(\mathcal{P})$, namely Definition 8.2. According to them, a transitive model $\mathcal{M} = (M; \in)$ is power admissible iff it satisfies $\operatorname{KP}^{\mathcal{P}}$, the extension of $\operatorname{KP}$ to formulae in $\mathcal L = \{ \in, \mathcal{P}\}$, interpreting, for any $x, y \in \mathcal{M}$, $$ \mathcal{P}^{\mathcal{M}}(x,y) \iff y \subseteq x. $$ It seems very likely to me that this is in fact the kind of structure Steel has in mind. However, since I am interested in some technical details of his constructions that rely on the precise properties of $\mathcal{M}$, I'd like to verify this educated guess.