src/ZF/Constructible/DPow_absolute.thy

 *)
 
 header {*Absoluteness for the Definable Powerset Function*}
 
 
-theory DPow_absolute = Satisfies_absolute:
+theory DPow_absolute imports Satisfies_absolute begin
 
 
 subsection{*Preliminary Internalizations*}
 
 subsubsection{*The Operator @{term is_formula_rec}*}