src/ZF/Constructible/Rec_Separation.thy

   done
 
 theorem M_trancl_L: "PROP M_trancl(L)"
 by (rule M_trancl.intro [OF M_basic_L M_trancl_axioms_L])
 
-interpretation L: M_trancl L by (rule M_trancl_L)
+interpretation L?: M_trancl L by (rule M_trancl_L)
 
 
 subsection{*@{term L} is Closed Under the Operator @{term list}*}
 
 subsubsection{*Instances of Replacement for Lists*}

   apply (rule M_datatypes.intro)
    apply (rule M_trancl_L)
   apply (rule M_datatypes_axioms_L) 
   done
 
-interpretation L: M_datatypes L by (rule M_datatypes_L)
+interpretation L?: M_datatypes L by (rule M_datatypes_L)
 
 
 subsection{*@{term L} is Closed Under the Operator @{term eclose}*}
 
 subsubsection{*Instances of Replacement for @{term eclose}*}

   apply (rule M_eclose.intro)
    apply (rule M_datatypes_L)
   apply (rule M_eclose_axioms_L)
   done
 
-interpretation L: M_eclose L by (rule M_eclose_L)
+interpretation L?: M_eclose L by (rule M_eclose_L)
 
 
 end